Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Continuity of Mappings over the Union of Subspaces

by
Zbigniew Karno

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;

```