The abstract of the Mizar article:

Continuity of Mappings over the Union of Subspaces

by

Zbigniew Karno

Received May 22, 1992

MML identifier: TMAP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, TARSKI, FUNCT_1, RELAT_1, BOOLE, FUNCT_4, SETFAM_1,
      SUBSET_1, CONNSP_2, ORDINAL2, FUNCOP_1, FUNCT_3, TSEP_1, CONNSP_1,
      TMAP_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, FUNCT_4, PRE_TOPC, CONNSP_2, BORSUK_1, GRCAT_1,
      TSEP_1;
 constructors TOPS_2, CONNSP_1, BORSUK_1, TSEP_1, GRCAT_1, PARTFUN1, MEMBERED,
      RELAT_2, XBOOLE_0;
 clusters FUNCT_1, PRE_TOPC, BORSUK_1, TSEP_1, STRUCT_0, COMPLSP1, RELSET_1,
      SUBSET_1, XBOOLE_0, ZFMISC_1, FUNCT_2, PARTFUN1;
 requirements BOOLE, SUBSET;


begin
::1. Set-Theoretic Preliminaries.

definition let X be non empty TopSpace;
           let X1, X2 be non empty SubSpace of X;
  cluster X1 union X2 -> TopSpace-like;
end;

reserve A,B for non empty set;

theorem :: TMAP_1:1
 for f being Function of A,B, A0 being Subset of A,
     B0 being Subset of B
  holds f.:A0 c= B0 iff A0 c= f"B0;

theorem :: TMAP_1:2
 for f being Function of A,B, A0 being non empty Subset of A,
  f0 being Function of A0,B st
   for c being Element of A st c in A0 holds f.c = f0.c
    holds f|A0 = f0;

canceled;

theorem :: TMAP_1:4
 for f being Function of A,B, A0 being non empty Subset of A,
  C being Subset of A st C c= A0 holds f.:C = (f|A0).:C;

theorem :: TMAP_1:5
 for f being Function of A,B, A0 being non empty Subset of A,
  D being Subset of B st f"D c= A0 holds f"D = (f|A0)"D;

definition let A,B be non empty set;
  let A1,A2 be non empty Subset of A;
            let f1 be Function of A1,B, f2 be Function of A2,B;
 assume
     f1|(A1 /\ A2) = f2|(A1 /\ A2);
 func f1 union f2 -> Function of A1 \/ A2,B means
:: TMAP_1:def 1
 it|A1 = f1 & it|A2 = f2;
end;

theorem :: TMAP_1:6
 for A, B be non empty set, A1, A2 being non empty Subset of A
    st A1 misses A2
  for f1 being Function of A1,B, f2 being Function of A2,B holds
   f1|(A1 /\ A2) = f2|(A1 /\
 A2) & (f1 union f2)|A1 = f1 & (f1 union f2)|A2 = f2;

reserve A, B for non empty set,
        A1, A2, A3 for non empty Subset of A;

theorem :: TMAP_1:7
 for g being Function of A1 \/ A2,B,
  g1 being Function of A1,B, g2 being Function of A2,B st
   g|A1 = g1 & g|A2 = g2 holds g = g1 union g2;

theorem :: TMAP_1:8
   for f1 being Function of A1,B, f2 being Function of A2,B st
  f1|(A1 /\ A2) = f2|(A1 /\ A2) holds f1 union f2 = f2 union f1;

theorem :: TMAP_1:9
   for A12, A23 being non empty Subset of A
    st A12 = A1 \/ A2 & A23 = A2 \/ A3
  for f1 being Function of A1,B, f2 being Function of A2,B,
   f3 being Function of A3,B st f1|(A1 /\ A2) = f2|(A1 /\ A2) &
    f2|(A2 /\ A3) = f3|(A2 /\ A3) & f1|(A1 /\ A3) = f3|(A1 /\ A3)
     for f12 being Function of A12,B, f23 being Function of A23,B st
      f12 = f1 union f2 & f23 = f2 union f3 holds f12 union f3 = f1 union f23;

theorem :: TMAP_1:10
   for f1 being Function of A1,B, f2 being Function of A2,B st
  f1|(A1 /\ A2) = f2|(A1 /\ A2) holds
   (A1 is Subset of A2 iff f1 union f2 = f2) &
     (A2 is Subset of A1 iff f1 union f2 = f1);

begin
::2. Selected Properties of Subspaces of Topological Spaces.
reserve X for non empty TopSpace;

theorem :: TMAP_1:11
 for X0 being non empty SubSpace of X
 holds the TopStruct of X0 is strict SubSpace of X;

theorem :: TMAP_1:12
 for X1,X2 being non empty TopSpace st X1 = the TopStruct of X2 holds
  X1 is SubSpace of X iff X2 is SubSpace of X;

theorem :: TMAP_1:13
 for X1,X2 be non empty TopSpace st X2 = the TopStruct of X1 holds
  X1 is closed SubSpace of X iff X2 is closed SubSpace of X;

theorem :: TMAP_1:14
 for X1,X2 be non empty TopSpace st X2 = the TopStruct of X1 holds
  X1 is open SubSpace of X iff X2 is open SubSpace of X;

reserve X1, X2 for non empty SubSpace of X;

theorem :: TMAP_1:15
 X1 is SubSpace of X2 implies
  for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1;

theorem :: TMAP_1:16
 for x being Point of X1 union X2 holds
  (ex x1 being Point of X1 st x1 = x) or (ex x2 being Point of X2 st x2 = x);

theorem :: TMAP_1:17
 X1 meets X2 implies
  for x being Point of X1 meet X2 holds
   (ex x1 being Point of X1 st x1 = x) & (ex x2 being Point of X2 st x2 = x);

theorem :: TMAP_1:18
   for x being Point of X1 union X2
  for F1 being Subset of X1,
      F2 being Subset of X2 st
   F1 is closed & x in F1 & F2 is closed & x in F2
    ex H being Subset of X1 union X2
    st H is closed & x in H & H c= F1 \/ F2;

theorem :: TMAP_1:19
 for x being Point of X1 union X2
  for U1 being Subset of X1,
      U2 being Subset of X2 st
   U1 is open & x in U1 & U2 is open & x in U2
    ex V being Subset of X1 union X2
    st V is open & x in V & V c= U1 \/ U2;

theorem :: TMAP_1:20
 for x being Point of X1 union X2
  for x1 being Point of X1, x2 being Point of X2 st x1 = x & x2 = x
   for A1 being a_neighborhood of x1, A2 being a_neighborhood of x2
    ex V being Subset of X1 union X2
     st V is open & x in V & V c= A1 \/ A2;

theorem :: TMAP_1:21
 for x being Point of X1 union X2
  for x1 being Point of X1, x2 being Point of X2 st x1 = x & x2 = x
   for A1 being a_neighborhood of x1, A2 being a_neighborhood of x2
    ex A being a_neighborhood of x st A c= A1 \/ A2;

reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X;

theorem :: TMAP_1:22
 X0 is SubSpace of X1 implies X0 meets X1 & X1 meets X0;

theorem :: TMAP_1:23
 X0 is SubSpace of X1 & (X0 meets X2 or X2 meets X0) implies
  X1 meets X2 & X2 meets X1;

theorem :: TMAP_1:24
 X0 is SubSpace of X1 & (X1 misses X2 or X2 misses X1) implies
  X0 misses X2 & X2 misses X0;

theorem :: TMAP_1:25
   X0 union X0 = the TopStruct of X0;

theorem :: TMAP_1:26
   X0 meet X0 = the TopStruct of X0;

theorem :: TMAP_1:27
 Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies
  Y1 union Y2 is SubSpace of X1 union X2;

theorem :: TMAP_1:28
   Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies
  Y1 meet Y2 is SubSpace of X1 meet X2;

theorem :: TMAP_1:29
 X1 is SubSpace of X0 & X2 is SubSpace of X0 implies
  X1 union X2 is SubSpace of X0;

theorem :: TMAP_1:30
   X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies
  X1 meet X2 is SubSpace of X0;

theorem :: TMAP_1:31
 ((X1 misses X0 or X0 misses X1) & (X2 meets X0 or X0 meets X2) implies
  (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2) &
  ((X1 meets X0 or X0 meets X1) & (X2 misses X0 or X0 misses X2) implies
    (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1);

theorem :: TMAP_1:32
 X1 meets X2 implies
 (X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2) &
  (X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0);

theorem :: TMAP_1:33
 X1 is SubSpace of X0 & (X0 misses X2 or X2 misses X0) implies
  X0 meet (X1 union X2) = the TopStruct of X1 &
   X0 meet (X2 union X1) = the TopStruct of X1;

theorem :: TMAP_1:34
 X1 meets X2 implies
 (X1 is SubSpace of X0 implies (X0 meet X2) meets X1 & (X2 meet X0) meets X1) &
  (X2 is SubSpace of X0 implies (X1 meet X0) meets X2 & (X0 meet X1) meets X2);

theorem :: TMAP_1:35
 X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
  (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2) implies
    Y1 misses X2 & Y2 misses X1;

theorem :: TMAP_1:36
 X1 is not SubSpace of X2 & X2 is not SubSpace of X1 &
  X1 union X2 is SubSpace of Y1 union Y2 &
   Y1 meet (X1 union X2) is SubSpace of X1 &
    Y2 meet (X1 union X2) is SubSpace of X2 implies
     Y1 meets X1 union X2 & Y2 meets X1 union X2;

theorem :: TMAP_1:37
 X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 &
  the TopStruct of X = (Y1 union Y2) union X0 &
   Y1 meet (X1 union X2) is SubSpace of X1 &
    Y2 meet (X1 union X2) is SubSpace of X2 &
     X0 meet (X1 union X2) is SubSpace of X1 meet X2 implies
      Y1 meets X1 union X2 & Y2 meets X1 union X2;

theorem :: TMAP_1:38
 X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 &
  not X1 union X2 is SubSpace of Y1 union Y2 &
  the TopStruct of X = (Y1 union Y2) union X0 &
   Y1 meet (X1 union X2) is SubSpace of X1 &
    Y2 meet (X1 union X2) is SubSpace of X2 &
     X0 meet (X1 union X2) is SubSpace of X1 meet X2 implies
      Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2;

theorem :: TMAP_1:39
 ((X1 union X2) meets X0 iff X1 meets X0 or X2 meets X0) &
  (X0 meets (X1 union X2) iff X0 meets X1 or X0 meets X2);

theorem :: TMAP_1:40
   ((X1 union X2) misses X0 iff X1 misses X0 & X2 misses X0) &
   (X0 misses (X1 union X2) iff X0 misses X1 & X0 misses X2);

theorem :: TMAP_1:41
   X1 meets X2 implies
  ((X1 meet X2) meets X0 implies X1 meets X0 & X2 meets X0) &
   (X0 meets (X1 meet X2) implies X0 meets X1 & X0 meets X2);

theorem :: TMAP_1:42
   X1 meets X2 implies
  (X1 misses X0 or X2 misses X0 implies (X1 meet X2) misses X0) &
   (X0 misses X1 or X0 misses X2 implies X0 misses (X1 meet X2));

theorem :: TMAP_1:43
 for X0 being closed non empty SubSpace of X holds
  X0 meets X1 implies X0 meet X1 is closed SubSpace of X1;

theorem :: TMAP_1:44
 for X0 being open non empty SubSpace of X holds
  X0 meets X1 implies X0 meet X1 is open SubSpace of X1;

theorem :: TMAP_1:45
   for X0 being closed non empty SubSpace of X holds
  X1 is SubSpace of X0 & X0 misses X2 implies
   X1 is closed SubSpace of X1 union X2 &
    X1 is closed SubSpace of X2 union X1;

theorem :: TMAP_1:46
 for X0 being open non empty SubSpace of X holds
  X1 is SubSpace of X0 & X0 misses X2 implies
   X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1;

begin
::3. Continuity of Mappings.

definition
 let X, Y be non empty TopSpace, f be map of X,Y, x be Point of X;
 pred f is_continuous_at x means
:: TMAP_1:def 2
 for G being a_neighborhood of f.x
  ex H being a_neighborhood of x st f.:H c= G;
 antonym f is_not_continuous_at x;
end;

reserve X, Y for non empty TopSpace; reserve f for map of X,Y;

theorem :: TMAP_1:47
 for x being Point of X holds
  f is_continuous_at x iff
   for G being a_neighborhood of f.x holds f"G is a_neighborhood of x;

theorem :: TMAP_1:48
 for x being Point of X holds
  f is_continuous_at x iff
   for G being Subset of Y st G is open & f.x in G
    ex H being Subset of X st H is open & x in H & f.:H c= G;

theorem :: TMAP_1:49
 f is continuous iff for x being Point of X holds f is_continuous_at x;

theorem :: TMAP_1:50
 for X,Y,Z being non empty TopSpace st
  the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y
   for f being map of X,Y, g being map of X,Z st f = g holds
    for x being Point of X holds
     f is_continuous_at x implies g is_continuous_at x;

theorem :: TMAP_1:51
 for X,Y,Z being non empty TopSpace st
  the carrier of X = the carrier of Y & the topology of Y c= the topology of X
   for f being map of X,Z, g being map of Y,Z st f = g holds
    for x being Point of X, y being Point of Y st x = y holds
     g is_continuous_at y implies f is_continuous_at x;

reserve X,Y,Z for non empty TopSpace;
reserve f for map of X,Y, g for map of Y,Z;

theorem :: TMAP_1:52
 for x being Point of X, y being Point of Y st y = f.x holds
  f is_continuous_at x & g is_continuous_at y implies g*f is_continuous_at x;

theorem :: TMAP_1:53
   for y being Point of Y holds
  f is continuous & g is_continuous_at y implies
   for x being Point of X st x in f"{y} holds g*f is_continuous_at x;

theorem :: TMAP_1:54
   for x being Point of X holds
  f is_continuous_at x & g is continuous implies g*f is_continuous_at x;

theorem :: TMAP_1:55
  f is continuous map of X,Y iff
  for x being Point of X holds f is_continuous_at x;

theorem :: TMAP_1:56
 for X,Y,Z being non empty TopSpace st
  the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y
   for f being continuous map of X,Y holds f is continuous map of X,Z;

theorem :: TMAP_1:57
   for X,Y,Z being non empty TopSpace st
  the carrier of X = the carrier of Y & the topology of Y c= the topology of X
   for f being continuous map of Y,Z holds f is continuous map of X,Z;

::(Definition of the restriction mapping - general case.)
definition
 let X, Y be non empty TopSpace, X0 be SubSpace of X, f be map of X,Y;
 func f|X0 -> map of X0,Y equals
:: TMAP_1:def 3
 f|(the carrier of X0);
end;

reserve X, Y for non empty TopSpace, X0 for non empty SubSpace of X;
reserve f for map of X,Y;

theorem :: TMAP_1:58
 for x being Point of X st x in the carrier of X0 holds f.x = (f|X0).x;

theorem :: TMAP_1:59
 for f0 being map of X0,Y st
  for x being Point of X st x in the carrier of X0 holds f.x = f0.x
   holds f|X0 = f0;

theorem :: TMAP_1:60
 the TopStruct of X0 = the TopStruct of X implies f = f|X0;

theorem :: TMAP_1:61
 for A being Subset of X st A c= the carrier of X0
   holds f.:A = (f|X0).:A;

theorem :: TMAP_1:62
   for B being Subset of Y st f"B c= the carrier of X0
 holds f"B = (f|X0)"B;

theorem :: TMAP_1:63
 for g being map of X0,Y ex h being map of X,Y st h|X0 = g;

reserve f for map of X,Y, X0 for non empty SubSpace of X;

theorem :: TMAP_1:64
 for x being Point of X, x0 being Point of X0 st x = x0 holds
  f is_continuous_at x implies f|X0 is_continuous_at x0;

::Characterizations of Continuity at the Point by Local one.
theorem :: TMAP_1:65
 for A being Subset of X, x being Point of X,
 x0 being Point of X0 st
  A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
   f is_continuous_at x iff f|X0 is_continuous_at x0;

theorem :: TMAP_1:66
 for A being Subset of X, x being Point of X,
 x0 being Point of X0 st
  A is open & x in A & A c= the carrier of X0 & x = x0 holds
   f is_continuous_at x iff f|X0 is_continuous_at x0;

theorem :: TMAP_1:67
   for X0 being open non empty SubSpace of X, x being Point of X,
     x0 being Point of X0 st
  x = x0 holds f is_continuous_at x iff f|X0 is_continuous_at x0;

theorem :: TMAP_1:68
 for f being continuous map of X,Y, X0 being non empty SubSpace of X holds
  f|X0 is continuous map of X0,Y;

theorem :: TMAP_1:69
 for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X,
  f being map of X,Y, g being map of Y,Z holds (g*f)|X0 = g*(f|X0);

theorem :: TMAP_1:70
 for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X,
  g being map of Y,Z, f being map of X,Y st
   g is continuous & f|X0 is continuous holds (g*f)|X0 is continuous;

theorem :: TMAP_1:71
   for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X,
  g being continuous map of Y,Z, f being map of X,Y st
   f|X0 is continuous map of X0,Y holds
    (g*f)|X0 is continuous map of X0,Z;

::(Definition of the restriction mapping - special case.)
definition
 let X,Y be non empty TopSpace, X0, X1 be SubSpace of X, g be map of X0,Y;
  assume  X1 is SubSpace of X0;
 func g|X1 -> map of X1,Y equals
:: TMAP_1:def 4
 g|(the carrier of X1);
end;

reserve X, Y for non empty TopSpace, X0, X1 for non empty SubSpace of X;
reserve f for map of X,Y, g for map of X0,Y;

theorem :: TMAP_1:72
 X1 is SubSpace of X0 implies
  for x0 being Point of X0 st x0 in the carrier of X1 holds g.x0 = (g|X1).x0;

theorem :: TMAP_1:73
   X1 is SubSpace of X0 implies for g1 being map of X1,Y st
  for x0 being Point of X0 st x0 in the carrier of X1 holds g.x0 = g1.x0
   holds g|X1 = g1;

theorem :: TMAP_1:74
 g = g|X0;

theorem :: TMAP_1:75
 X1 is SubSpace of X0 implies
  for A being Subset of X0 st A c= the carrier of X1
  holds g.:A = (g|X1).:A;

theorem :: TMAP_1:76
   X1 is SubSpace of X0 implies
  for B being Subset of Y st g"B c= the carrier of X1
  holds g"B = (g|X1)"B;

theorem :: TMAP_1:77
 for g being map of X0,Y st g = f|X0 holds
  X1 is SubSpace of X0 implies g|X1 = f|X1;

theorem :: TMAP_1:78
 X1 is SubSpace of X0 implies (f|X0)|X1 = f|X1;

theorem :: TMAP_1:79
 for X0, X1, X2 being non empty SubSpace of X st
  X1 is SubSpace of X0 & X2 is SubSpace of X1
   for g being map of X0,Y holds (g|X1)|X2 = g|X2;

theorem :: TMAP_1:80
 for f being map of X,Y, f0 being map of X1,Y,
  g being map of X0,Y holds
   X0 = X & f = g implies (g|X1 = f0 iff f|X1 = f0);

reserve X0, X1, X2 for non empty SubSpace of X;
reserve f for map of X,Y, g for map of X0,Y;

theorem :: TMAP_1:81
 for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds
  X1 is SubSpace of X0 & g is_continuous_at x0 implies
   g|X1 is_continuous_at x1;

theorem :: TMAP_1:82
 X1 is SubSpace of X0 implies
  for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds
   f|X0 is_continuous_at x0 implies f|X1 is_continuous_at x1;

::Characterizations of Continuity at the Point by Local one.
theorem :: TMAP_1:83
 X1 is SubSpace of X0 implies
  for A being Subset of X0, x0 being Point of X0,
  x1 being Point of X1 st
   A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
    g is_continuous_at x0 iff g|X1 is_continuous_at x1;

theorem :: TMAP_1:84
 X1 is SubSpace of X0 implies
  for A being Subset of X0, x0 being Point of X0,
  x1 being Point of X1 st
   A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds
    g is_continuous_at x0 iff g|X1 is_continuous_at x1;

theorem :: TMAP_1:85
   X1 is SubSpace of X0 implies
  for A being Subset of X, x0 being Point of X0,
  x1 being Point of X1 st
   A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds
    g is_continuous_at x0 iff g|X1 is_continuous_at x1;

theorem :: TMAP_1:86
 X1 is open SubSpace of X0 implies
  for x0 being Point of X0, x1 being Point of X1 st
   x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1;

theorem :: TMAP_1:87
   X1 is open SubSpace of X & X1 is SubSpace of X0 implies
  for x0 being Point of X0, x1 being Point of X1 st
   x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1;

theorem :: TMAP_1:88
 the TopStruct of X1 = X0 implies
  for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds
   g|X1 is_continuous_at x1 implies g is_continuous_at x0;

theorem :: TMAP_1:89
 for g being continuous map of X0,Y holds
  X1 is SubSpace of X0 implies g|X1 is continuous map of X1,Y;

theorem :: TMAP_1:90
 X1 is SubSpace of X0 & X2 is SubSpace of X1 implies
  for g being map of X0,Y holds
 g|X1 is continuous map of X1,Y implies g|X2 is continuous map of X2,Y;

theorem :: TMAP_1:91
 for X being non empty 1-sorted, x being Element of X
   holds (id X).x = x;

theorem :: TMAP_1:92
   for X being non empty 1-sorted, f being map of X,X
   st for x being Element of X holds f.x = x
  holds f = id X;

theorem :: TMAP_1:93
 for X,Y being non empty 1-sorted,
     f being Function of the carrier of X,the carrier of Y
  holds f*(id X) = f & (id Y)*f = f;

theorem :: TMAP_1:94
 id X is continuous map of X,X;

::(Definition of the inclusion mapping.)
definition let X be non empty TopSpace, X0 be SubSpace of X;
 canceled;

 func incl X0 -> map of X0,X equals
:: TMAP_1:def 6
 (id X)|X0;
 synonym X0 incl X;
end;

theorem :: TMAP_1:95
   for X0 being non empty SubSpace of X, x being Point of X
   st x in the carrier of X0
  holds (incl X0).x = x;

theorem :: TMAP_1:96
   for X0 being non empty SubSpace of X, f0 being map of X0,X st
  for x being Point of X st x in the carrier of X0 holds x = f0.x
   holds incl X0 = f0;

theorem :: TMAP_1:97
   for X0 being non empty SubSpace of X, f being map of X,Y
   holds f|X0 = f*(incl X0);

theorem :: TMAP_1:98
   for X0 being non empty SubSpace of X
   holds incl X0 is continuous map of X0,X;


begin
::4. A Modification of the Topology of Topological Spaces.
reserve X for non empty TopSpace, H, G for Subset of X;

definition let X; let A be Subset of X;
 func A-extension_of_the_topology_of X -> Subset-Family of X equals
:: TMAP_1:def 7
 {H \/ (G /\ A) : H in the topology of X & G in the topology of X};
end;

theorem :: TMAP_1:99
 for A being Subset of X holds
  the topology of X c= A-extension_of_the_topology_of X;

theorem :: TMAP_1:100
 for A being Subset of X holds
  {G /\ A where G is Subset of X : G in the topology of X} c=
    A-extension_of_the_topology_of X;

theorem :: TMAP_1:101
 for A being Subset of X holds for C,
     D being Subset of X st
  C in the topology of X &
   D in {G /\ A where G is Subset of X :
   G in the topology of X} holds
    C \/ D in A-extension_of_the_topology_of X &
     C /\ D in A-extension_of_the_topology_of X;

theorem :: TMAP_1:102
 for A being Subset of X
   holds A in A-extension_of_the_topology_of X;

theorem :: TMAP_1:103
 for A being Subset of X holds A in the topology of X iff
  the topology of X = A-extension_of_the_topology_of X;

definition let X be non empty TopSpace, A be Subset of X;
 func X modified_with_respect_to A -> strict TopSpace equals
:: TMAP_1:def 8
 TopStruct(#the carrier of X, A-extension_of_the_topology_of X#);
end;

definition let X be non empty TopSpace, A be Subset of X;
 cluster X modified_with_respect_to A -> non empty;
end;

reserve A for Subset of X;

theorem :: TMAP_1:104
 the carrier of (X modified_with_respect_to A) = the carrier of X &
  the topology of (X modified_with_respect_to A) =
   A-extension_of_the_topology_of X;

theorem :: TMAP_1:105
 for B being Subset of X modified_with_respect_to A st B = A
   holds B is open;

theorem :: TMAP_1:106
 for A being Subset of X holds
  A is open iff the TopStruct of X = X modified_with_respect_to A;

definition let X be non empty TopSpace, A be Subset of X;
 func modid(X,A) -> map of X,X modified_with_respect_to A equals
:: TMAP_1:def 9
 id (the carrier of X);
end;

theorem :: TMAP_1:107
 for A being Subset of X st A is open holds modid(X,A) = id X;

theorem :: TMAP_1:108
 for x being Point of X st not x in A holds modid(X,A) is_continuous_at x;

theorem :: TMAP_1:109
 for X0 being non empty SubSpace of X st the carrier of X0 misses A
  for x0 being Point of X0 holds (modid(X,A))|X0 is_continuous_at x0;

theorem :: TMAP_1:110
 for X0 being non empty SubSpace of X st the carrier of X0 = A
  for x0 being Point of X0 holds (modid(X,A))|X0 is_continuous_at x0;

theorem :: TMAP_1:111
 for X0 being non empty SubSpace of X st the carrier of X0 misses A holds
  (modid(X,A))|X0 is continuous map of X0,X modified_with_respect_to A;

theorem :: TMAP_1:112
 for X0 being non empty SubSpace of X st the carrier of X0 = A holds
  (modid(X,A))|X0 is continuous map of X0,X modified_with_respect_to A;

theorem :: TMAP_1:113
 for A being Subset of X holds
  A is open iff
   modid(X,A) is continuous map of X,X modified_with_respect_to A;

definition let X be non empty TopSpace, X0 be SubSpace of X;
 func X modified_with_respect_to X0 -> strict TopSpace means
:: TMAP_1:def 10
 for A being Subset of X st A = the carrier of X0 holds
  it = X modified_with_respect_to A;
end;

definition let X be non empty TopSpace, X0 be SubSpace of X;
 cluster X modified_with_respect_to X0 -> non empty;
end;

reserve X0 for non empty SubSpace of X;

theorem :: TMAP_1:114
 the carrier of (X modified_with_respect_to X0) = the carrier of X &
  for A being Subset of X st A = the carrier of X0 holds
   the topology of (X modified_with_respect_to X0) =
    A-extension_of_the_topology_of X;

theorem :: TMAP_1:115
   for Y0 being SubSpace of X modified_with_respect_to X0 st
  the carrier of Y0 = the carrier of X0 holds
   Y0 is open SubSpace of X modified_with_respect_to X0;

theorem :: TMAP_1:116
   X0 is open SubSpace of X iff
  the TopStruct of X = X modified_with_respect_to X0;

definition let X be non empty TopSpace, X0 be SubSpace of X;
 func modid(X,X0) -> map of X,X modified_with_respect_to X0 means
:: TMAP_1:def 11
 for A being Subset of X st A = the carrier of X0 holds
  it = modid(X,A);
end;

theorem :: TMAP_1:117
   X0 is open SubSpace of X implies modid(X,X0) = id X;

theorem :: TMAP_1:118
 for X0, X1 being non empty SubSpace of X st X0 misses X1
  for x1 being Point of X1 holds (modid(X,X0))|X1 is_continuous_at x1;

theorem :: TMAP_1:119
 for X0 being non empty SubSpace of X
  for x0 being Point of X0 holds (modid(X,X0))|X0 is_continuous_at x0;

theorem :: TMAP_1:120
   for X0, X1 being non empty SubSpace of X st X0 misses X1 holds
  (modid(X,X0))|X1 is continuous map of X1,X modified_with_respect_to X0;

theorem :: TMAP_1:121
   for X0 being non empty SubSpace of X holds
  (modid(X,X0))|X0 is continuous map of X0,X modified_with_respect_to X0;

theorem :: TMAP_1:122
   for X0 being SubSpace of X holds
  X0 is open SubSpace of X iff
   modid(X,X0) is continuous map of X,X modified_with_respect_to X0;


begin
::5. Continuity of Mappings over the Union of Subspaces.
reserve X, Y for non empty TopSpace;

::Continuity at the Point of Mappings over the Union of Subspaces.
theorem :: TMAP_1:123
 for X1, X2 being non empty SubSpace of X, g being map of X1 union X2,Y
  for x1 being Point of X1, x2 being Point of X2,
   x being Point of X1 union X2 st x = x1 & x = x2 holds
    g is_continuous_at x iff
     g|X1 is_continuous_at x1 & g|X2 is_continuous_at x2;

theorem :: TMAP_1:124
   for f being map of X,Y, X1, X2 being non empty SubSpace of X
  for x being Point of X1 union X2,
   x1 being Point of X1, x2 being Point of X2 st x = x1 & x = x2 holds
    f|(X1 union X2) is_continuous_at x iff
     f|X1 is_continuous_at x1 & f|X2 is_continuous_at x2;

theorem :: TMAP_1:125
   for f being map of X,Y, X1, X2 being non empty SubSpace of X
   st X = X1 union X2
  for x being Point of X, x1 being Point of X1, x2 being Point of X2 st
   x = x1 & x = x2 holds
    f is_continuous_at x iff
     f|X1 is_continuous_at x1 & f|X2 is_continuous_at x2;

reserve X1, X2 for non empty SubSpace of X;

::Continuity of Mappings over the Union of Subspaces.
theorem :: TMAP_1:126
 X1,X2 are_weakly_separated implies
  for g being map of X1 union X2,Y holds
   g is continuous map of X1 union X2,Y iff
    g|X1 is continuous map of X1,Y & g|X2 is continuous map of X2,Y;

theorem :: TMAP_1:127
 for X1, X2 being closed non empty SubSpace of X
  for g being map of X1 union X2,Y holds
   g is continuous map of X1 union X2,Y iff
    g|X1 is continuous map of X1,Y & g|X2 is continuous map of X2,Y;

theorem :: TMAP_1:128
 for X1, X2 being open non empty SubSpace of X
  for g being map of X1 union X2,Y holds
   g is continuous map of X1 union X2,Y iff
    g|X1 is continuous map of X1,Y & g|X2 is continuous map of X2,Y;

theorem :: TMAP_1:129
 X1,X2 are_weakly_separated implies
  for f being map of X,Y holds
   f|(X1 union X2) is continuous map of X1 union X2,Y iff
    f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y;

theorem :: TMAP_1:130
   for f being map of X,Y, X1, X2 being closed non empty SubSpace of X holds
  f|(X1 union X2) is continuous map of X1 union X2,Y iff
   f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y;

theorem :: TMAP_1:131
   for f being map of X,Y, X1, X2 being open non empty SubSpace of X holds
  f|(X1 union X2) is continuous map of X1 union X2,Y iff
   f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y;

theorem :: TMAP_1:132
 for f being map of X,Y, X1, X2 being non empty SubSpace of X st
  X = X1 union X2 & X1,X2 are_weakly_separated holds
   f is continuous map of X,Y iff
    f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y;

theorem :: TMAP_1:133
 for f being map of X,Y, X1, X2 being closed non empty SubSpace of X st
  X = X1 union X2 holds
   f is continuous map of X,Y iff
    f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y;

theorem :: TMAP_1:134
 for f being map of X,Y, X1, X2 being open non empty SubSpace of X st
  X = X1 union X2 holds
   f is continuous map of X,Y iff
    f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y;

::Some Characterizations of Separated Subspaces of Topological Spaces.
theorem :: TMAP_1:135
 X1,X2 are_separated iff X1 misses X2 &
  for Y being non empty TopSpace, g being map of X1 union X2,Y st
   g|X1 is continuous map of X1,Y & g|X2 is continuous map of X2,Y
    holds g is continuous map of X1 union X2,Y;

theorem :: TMAP_1:136
 X1,X2 are_separated iff X1 misses X2 &
  for Y being non empty TopSpace, f being map of X,Y st
   f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y
    holds f|(X1 union X2) is continuous map of X1 union X2,Y;

theorem :: TMAP_1:137
   for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds
  X1,X2 are_separated iff X1 misses X2 &
   for Y being non empty TopSpace, f being map of X,Y st
    f|X1 is continuous map of X1,Y & f|X2 is continuous map of X2,Y
     holds f is continuous map of X,Y;


begin
::6. The Union of Continuous Mappings.

definition let X,Y be non empty TopSpace, X1, X2 be non empty SubSpace of X;
            let f1 be map of X1,Y, f2 be map of X2,Y;
 assume X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2);
   func f1 union f2 -> map of X1 union X2,Y means
:: TMAP_1:def 12
 it|X1 = f1 & it|X2 = f2;
end;

reserve X, Y for non empty TopSpace;

theorem :: TMAP_1:138
 for X1, X2 being non empty SubSpace of X
  for g being map of X1 union X2,Y holds g = (g|X1) union (g|X2);

theorem :: TMAP_1:139
   for X1, X2 being non empty SubSpace of X st X = X1 union X2
  for g being map of X,Y holds g = (g|X1) union (g|X2);

theorem :: TMAP_1:140
 for X1, X2 being non empty SubSpace of X st X1 meets X2
  for f1 being map of X1,Y, f2 being map of X2,Y holds
   (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 iff
     f1|(X1 meet X2) = f2|(X1 meet X2);

theorem :: TMAP_1:141
   for X1, X2 being non empty SubSpace of X,
  f1 being map of X1,Y, f2 being map of X2,Y st
   f1|(X1 meet X2) = f2|(X1 meet X2) holds
    (X1 is SubSpace of X2 iff f1 union f2 = f2) &
     (X2 is SubSpace of X1 iff f1 union f2 = f1);

theorem :: TMAP_1:142
   for X1, X2 being non empty SubSpace of X,
  f1 being map of X1,Y, f2 being map of X2,Y st
   X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2) holds
    f1 union f2 = f2 union f1;

theorem :: TMAP_1:143
   for X1, X2, X3 being non empty SubSpace of X,
  f1 being map of X1,Y, f2 being map of X2,Y, f3 being map of X3,Y
   st (X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2)) &
       (X1 misses X3 or f1|(X1 meet X3) = f3|(X1 meet X3)) &
        (X2 misses X3 or f2|(X2 meet X3) = f3|(X2 meet X3)) holds
      (f1 union f2) union f3 = f1 union (f2 union f3);

::Continuity of the Union of Continuous Mappings.
::(Theorems presented below are suitable also in the case X = X1 union X2.)
theorem :: TMAP_1:144
   for X1, X2 being non empty SubSpace of X st X1 meets X2
  for f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
   st f1|(X1 meet X2) = f2|(X1 meet X2) holds
    X1,X2 are_weakly_separated implies
     f1 union f2 is continuous map of X1 union X2,Y;

theorem :: TMAP_1:145
 for X1, X2 being non empty SubSpace of X st X1 misses X2
  for f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
   holds X1,X2 are_weakly_separated implies
    f1 union f2 is continuous map of X1 union X2,Y;

theorem :: TMAP_1:146
   for X1, X2 being closed non empty SubSpace of X st X1 meets X2
  for f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
   st f1|(X1 meet X2) = f2|(X1 meet X2) holds
    f1 union f2 is continuous map of X1 union X2,Y;

theorem :: TMAP_1:147
   for X1, X2 being open non empty SubSpace of X st X1 meets X2
  for f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
   st f1|(X1 meet X2) = f2|(X1 meet X2) holds
    f1 union f2 is continuous map of X1 union X2,Y;

theorem :: TMAP_1:148
   for X1, X2 being closed non empty SubSpace of X st X1 misses X2
  for f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
   holds f1 union f2 is continuous map of X1 union X2,Y;

theorem :: TMAP_1:149
   for X1, X2 being open non empty SubSpace of X st X1 misses X2
  for f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
   holds f1 union f2 is continuous map of X1 union X2,Y;

::A Characterization of Separated Subspaces by means of Continuity of the Union
::of Continuous continuous mappings defined on the Subspaces.
theorem :: TMAP_1:150
   for X1, X2 being non empty SubSpace of X holds X1,X2 are_separated iff
  X1 misses X2 & for Y being non empty TopSpace,
   f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
    holds f1 union f2 is continuous map of X1 union X2,Y;

::Continuity of the Union of Continuous Mappings (a special case).
theorem :: TMAP_1:151
   for X1, X2 being non empty SubSpace of X st X = X1 union X2
  for f1 being continuous map of X1,Y, f2 being continuous map of X2,Y
   st (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds
  X1,X2 are_weakly_separated implies f1 union f2 is continuous map of X,Y;

theorem :: TMAP_1:152
   for X1, X2 being closed non empty SubSpace of X,
  f1 being continuous map of X1,Y, f2 being continuous map of X2,Y st
   X = X1 union X2 & (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds
    f1 union f2 is continuous map of X,Y;

theorem :: TMAP_1:153
   for X1, X2 being open non empty SubSpace of X,
  f1 being continuous map of X1,Y, f2 being continuous map of X2,Y st
   X = X1 union X2 & (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds
    f1 union f2 is continuous map of X,Y;