:: Continuity of Mappings over the Union of Subspaces
:: by Zbigniew Karno
::
:: Received May 22, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PRE_TOPC, TARSKI, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4,
STRUCT_0, RCOMP_1, SETFAM_1, CONNSP_2, ORDINAL2, FUNCOP_1, FUNCT_3,
ZFMISC_1, TSEP_1, CONNSP_1, TMAP_1, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, DOMAIN_1, STRUCT_0, PRE_TOPC,
CONNSP_1, CONNSP_2, BORSUK_1, TSEP_1;
constructors SETFAM_1, FUNCT_4, CONNSP_1, BORSUK_1, TSEP_1, FUNCOP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC,
BORSUK_1, TSEP_1, RELSET_1, PARTFUN1, TOPS_1;
requirements BOOLE, SUBSET;
begin :: 1. Set-Theoretic Preliminaries.
registration
let X be non empty TopSpace;
let X1, X2 be non empty SubSpace of X;
cluster X1 union X2 -> TopSpace-like;
end;
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;
func f1 union f2 -> Function of A1 \/ A2,B equals
:: TMAP_1:def 1
f1 +* f2;
end;
theorem :: TMAP_1:1
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:2
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:3
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:4
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:5
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 TopSpace;
theorem :: TMAP_1:6
for X being TopStruct, X0 being SubSpace of X holds
the TopStruct of X0 is strict SubSpace of X;
theorem :: TMAP_1:7
for X being TopStruct for X1,X2 being TopSpace st
X1 = the TopStruct of X2 holds X1 is SubSpace of X iff X2 is SubSpace of X;
theorem :: TMAP_1:8
for X1,X2 being TopSpace st X2 = the TopStruct of X1 holds
X1 is closed SubSpace of X iff X2 is closed SubSpace of X;
theorem :: TMAP_1:9
for X1,X2 being TopSpace st X2 = the TopStruct of X1 holds
X1 is open SubSpace of X iff X2 is open SubSpace of X;
reserve X for non empty TopSpace;
reserve X1, X2 for non empty SubSpace of X;
theorem :: TMAP_1:10
X1 is SubSpace of X2 implies for x1 being Point of X1
ex x2 being Point of X2 st x2 = x1;
theorem :: TMAP_1:11
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:12
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:13
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:14
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:15
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:16
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:17
X0 is SubSpace of X1 implies X0 meets X1 & X1 meets X0;
theorem :: TMAP_1:18
X0 is SubSpace of X1 & (X0 meets X2 or X2 meets X0) implies X1
meets X2 & X2 meets X1;
theorem :: TMAP_1:19
X0 is SubSpace of X1 & (X1 misses X2 or X2 misses X1) implies X0
misses X2 & X2 misses X0;
theorem :: TMAP_1:20
X0 union X0 = the TopStruct of X0;
theorem :: TMAP_1:21
X0 meet X0 = the TopStruct of X0;
theorem :: TMAP_1:22
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies Y1 union Y2
is SubSpace of X1 union X2;
theorem :: TMAP_1:23
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:24
X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 union X2
is SubSpace of X0;
theorem :: TMAP_1:25
X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1
meet X2 is SubSpace of X0;
theorem :: TMAP_1:26
((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:27
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:28
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:29
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:30
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:31
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:32
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:33
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:34
((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:35
((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:36
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:37
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:38
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:39
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:40
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:41
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 Function 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;
end;
notation
let X, Y be non empty TopSpace, f be Function of X,Y, x be Point of X;
antonym f is_not_continuous_at x for f is_continuous_at x;
end;
reserve X, Y for non empty TopSpace;
reserve f for Function of X,Y;
theorem :: TMAP_1:42
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:43
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:44
f is continuous iff for x being Point of X holds f is_continuous_at x;
theorem :: TMAP_1:45
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 Function of X
,Y, g being Function 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:46
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 Function of X
,Z, g being Function 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 Function of X,Y,
g for Function of Y,Z;
theorem :: TMAP_1:47
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:48
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:49
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:50
f is continuous Function of X,Y iff for x being Point of X holds f
is_continuous_at x;
theorem :: TMAP_1:51
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
Function of X,Y holds f is continuous Function of X,Z;
theorem :: TMAP_1:52
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 Function
of Y,Z holds f is continuous Function of X,Z;
definition
let S,T be 1-sorted;
let f be Function of S,T;
let R be 1-sorted such that
the carrier of R c= the carrier of S;
func f|R -> Function of R,T equals
:: TMAP_1:def 3
f | the carrier of R;
end;
definition
let X, Y be non empty TopSpace, f be Function of X,Y;
let X0 be SubSpace of X;
redefine func f | X0 equals
:: TMAP_1:def 4
f | the carrier of X0;
end;
reserve X, Y for non empty TopSpace,
X0 for non empty SubSpace of X;
reserve f for Function of X,Y;
theorem :: TMAP_1:53
for f0 being Function 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:54
the TopStruct of X0 = the TopStruct of X implies f = f|X0;
theorem :: TMAP_1:55
for A being Subset of X st A c= the carrier of X0 holds f.:A = (f|X0)
.:A;
theorem :: TMAP_1:56
for B being Subset of Y st f"B c= the carrier of X0 holds f"B = (f|X0)
"B;
theorem :: TMAP_1:57
for g being Function of X0,Y ex h being Function of X,Y st h|X0 = g;
reserve f for Function of X,Y,
X0 for non empty SubSpace of X;
theorem :: TMAP_1:58
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:59
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:60
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:61
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;
registration let X,Y;
let f be continuous Function of X,Y, X0 be non empty SubSpace of X;
cluster f|X0 -> continuous;
end;
theorem :: TMAP_1:62
for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace
of X, f being Function of X,Y, g being Function of Y,Z holds (g*f)|X0 = g*(f|X0
);
theorem :: TMAP_1:63
for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace
of X, g being Function of Y,Z, f being Function of X,Y st g is continuous & f|
X0 is continuous holds (g*f)|X0 is continuous;
theorem :: TMAP_1:64
for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X,
g being continuous Function of Y,Z, f being Function of X,Y st f|X0 is
continuous Function of X0,Y holds (g*f)|X0 is continuous Function 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 Function of X0,
Y;
assume
X1 is SubSpace of X0;
func g|X1 -> Function of X1,Y equals
:: TMAP_1:def 5
g | the carrier of X1;
end;
reserve X, Y for non empty TopSpace,
X0, X1 for non empty SubSpace of X;
reserve f for Function of X,Y,
g for Function of X0,Y;
theorem :: TMAP_1:65
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:66
X1 is SubSpace of X0 implies for g1 being Function 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:67
g = g|X0;
theorem :: TMAP_1:68
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:69
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:70
for g being Function of X0,Y st g = f|X0 holds X1 is SubSpace of
X0 implies g|X1 = f|X1;
theorem :: TMAP_1:71
X1 is SubSpace of X0 implies (f|X0)|X1 = f|X1;
theorem :: TMAP_1:72
for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace
of X0 & X2 is SubSpace of X1 for g being Function of X0,Y holds (g|X1)|X2 = g|
X2;
theorem :: TMAP_1:73
for f being Function of X,Y, f0 being Function of X1,Y, g being
Function 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 Function of X,Y,
g for Function of X0,Y;
theorem :: TMAP_1:74
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:75
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:76
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:77
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:78
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:79
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:80
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:81
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:82
for g being continuous Function of X0,Y holds X1 is SubSpace of
X0 implies g|X1 is continuous Function of X1,Y;
theorem :: TMAP_1:83
X1 is SubSpace of X0 & X2 is SubSpace of X1 implies for g being
Function of X0,Y holds g|X1 is continuous Function of X1,Y implies g|X2 is
continuous Function of X2,Y;
registration let X;
cluster id X -> continuous;
end;
::(Definition of the inclusion mapping.)
definition
let X be non empty TopSpace, X0 be SubSpace of X;
func incl X0 -> Function of X0,X equals
:: TMAP_1:def 6
(id X)|X0;
end;
notation
let X be non empty TopSpace, X0 be SubSpace of X;
synonym X0 incl X for incl X0;
end;
theorem :: TMAP_1:84
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:85
for X0 being non empty SubSpace of X, f0 being Function 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:86
for X0 being non empty SubSpace of X, f being Function of X,Y holds f|
X0 = f*(incl X0);
theorem :: TMAP_1:87
for X0 being non empty SubSpace of X holds incl X0 is continuous
Function 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:88
for A being Subset of X holds the topology of X c= A
-extension_of_the_topology_of X;
theorem :: TMAP_1:89
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:90
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:91
for A being Subset of X holds A in A -extension_of_the_topology_of X;
theorem :: TMAP_1:92
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;
registration
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:93
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:94
for B being Subset of X modified_with_respect_to A st B = A holds B is open;
theorem :: TMAP_1:95
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) -> Function of X,X modified_with_respect_to A equals
:: TMAP_1:def 9
id (the
carrier of X);
end;
theorem :: TMAP_1:96
for x being Point of X st not x in A holds modid(X,A) is_continuous_at x;
theorem :: TMAP_1:97
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:98
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:99
for X0 being non empty SubSpace of X st the carrier of X0
misses A holds (modid(X,A))|X0 is continuous Function of X0,X
modified_with_respect_to A;
theorem :: TMAP_1:100
for X0 being non empty SubSpace of X st the carrier of X0 = A
holds (modid(X,A))|X0 is continuous Function of X0,X modified_with_respect_to A
;
theorem :: TMAP_1:101
for A being Subset of X holds A is open iff modid(X,A) is
continuous Function 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;
registration
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:102
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:103
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:104
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) -> Function 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:105
modid(X,X0) = id X;
theorem :: TMAP_1:106
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:107
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:108
for X0, X1 being non empty SubSpace of X st X0 misses X1 holds (modid(
X,X0))|X1 is continuous Function of X1,X modified_with_respect_to X0;
theorem :: TMAP_1:109
for X0 being non empty SubSpace of X holds (modid(X,X0))|X0 is
continuous Function of X0,X modified_with_respect_to X0;
theorem :: TMAP_1:110
for X0 being SubSpace of X holds X0 is open SubSpace of X iff modid(X,
X0) is continuous Function 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:111
for X1, X2 being non empty SubSpace of X, g being Function 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:112
for f being Function 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:113
for f being Function 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:114
X1,X2 are_weakly_separated implies for g being Function of X1
union X2,Y holds g is continuous Function of X1 union X2,Y iff g|X1 is
continuous Function of X1,Y & g|X2 is continuous Function of X2,Y;
theorem :: TMAP_1:115
for X1, X2 being closed non empty SubSpace of X for g being
Function of X1 union X2,Y holds g is continuous Function of X1 union X2,Y iff g
|X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y;
theorem :: TMAP_1:116
for X1, X2 being open non empty SubSpace of X for g being
Function of X1 union X2,Y holds g is continuous Function of X1 union X2,Y iff g
|X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y;
theorem :: TMAP_1:117
X1,X2 are_weakly_separated implies for f being Function of X,Y
holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is
continuous Function of X1,Y & f|X2 is continuous Function of X2,Y;
theorem :: TMAP_1:118
for f being Function of X,Y, X1, X2 being closed non empty SubSpace of
X holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is
continuous Function of X1,Y & f|X2 is continuous Function of X2,Y;
theorem :: TMAP_1:119
for f being Function of X,Y, X1, X2 being open non empty SubSpace of X
holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is
continuous Function of X1,Y & f|X2 is continuous Function of X2,Y;
theorem :: TMAP_1:120
for f being Function 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
Function of X,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous
Function of X2,Y;
theorem :: TMAP_1:121
for f being Function of X,Y, X1, X2 being closed non empty
SubSpace of X st X = X1 union X2 holds f is continuous Function of X,Y iff f|X1
is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y;
theorem :: TMAP_1:122
for f being Function of X,Y, X1, X2 being open non empty
SubSpace of X st X = X1 union X2 holds f is continuous Function of X,Y iff f|X1
is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y;
::Some Characterizations of Separated Subspaces of Topological Spaces.
theorem :: TMAP_1:123
X1,X2 are_separated iff X1 misses X2 & for Y being non empty
TopSpace, g being Function of X1 union X2,Y st g|X1 is continuous Function of
X1,Y & g|X2 is continuous Function of X2,Y holds g is continuous Function of X1
union X2,Y;
theorem :: TMAP_1:124
X1,X2 are_separated iff X1 misses X2 & for Y being non empty
TopSpace, f being Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2
is continuous Function of X2,Y holds f|(X1 union X2) is continuous Function of
X1 union X2,Y;
theorem :: TMAP_1:125
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
Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2 is continuous
Function of X2,Y holds f is continuous Function 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 Function of X1,Y, f2 be Function of X2,Y;
assume
X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2);
func f1 union f2 -> Function 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:126
for X1, X2 being non empty SubSpace of X for g being Function
of X1 union X2,Y holds g = (g|X1) union (g|X2);
theorem :: TMAP_1:127
for X1, X2 being non empty SubSpace of X st X = X1 union X2 for g
being Function of X,Y holds g = (g|X1) union (g|X2);
theorem :: TMAP_1:128
for X1, X2 being non empty SubSpace of X st X1 meets X2 for f1
being Function of X1,Y, f2 being Function 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:129
for X1, X2 being non empty SubSpace of X, f1 being Function of X1,Y,
f2 being Function 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:130
for X1, X2 being non empty SubSpace of X, f1 being Function of X1,Y,
f2 being Function 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:131
for X1, X2, X3 being non empty SubSpace of X, f1 being Function of X1,
Y, f2 being Function of X2,Y, f3 being Function 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:132
for X1, X2 being non empty SubSpace of X st X1 meets X2 for f1 being
continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|(X1
meet X2) = f2|(X1 meet X2) holds X1,X2 are_weakly_separated implies f1 union f2
is continuous Function of X1 union X2,Y;
theorem :: TMAP_1:133
for X1, X2 being non empty SubSpace of X st X1 misses X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds
X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of X1
union X2,Y;
theorem :: TMAP_1:134
for X1, X2 being closed non empty SubSpace of X st X1 meets X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|(
X1 meet X2) = f2|(X1 meet X2) holds f1 union f2 is continuous Function of X1
union X2,Y;
theorem :: TMAP_1:135
for X1, X2 being open non empty SubSpace of X st X1 meets X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|(
X1 meet X2) = f2|(X1 meet X2) holds f1 union f2 is continuous Function of X1
union X2,Y;
theorem :: TMAP_1:136
for X1, X2 being closed non empty SubSpace of X st X1 misses X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds
f1 union f2 is continuous Function of X1 union X2,Y;
theorem :: TMAP_1:137
for X1, X2 being open non empty SubSpace of X st X1 misses X2 for f1
being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds
f1 union f2 is continuous Function 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:138
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 Function of
X1,Y, f2 being continuous Function of X2,Y holds f1 union f2 is continuous
Function of X1 union X2,Y;
::Continuity of the Union of Continuous Mappings (a special case).
theorem :: TMAP_1:139
for X1, X2 being non empty SubSpace of X st X = X1 union X2 for f1
being continuous Function of X1,Y, f2 being continuous Function 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 Function of X,Y;
theorem :: TMAP_1:140
for X1, X2 being closed non empty SubSpace of X, f1 being continuous
Function of X1,Y, f2 being continuous Function of X2,Y st X = X1 union X2 & (f1
union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds f1 union f2 is continuous
Function of X,Y;
theorem :: TMAP_1:141
for X1, X2 being open non empty SubSpace of X, f1 being continuous
Function of X1,Y, f2 being continuous Function of X2,Y st X = X1 union X2 & (f1
union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds f1 union f2 is continuous
Function of X,Y;
theorem :: TMAP_1:142
for A,B be non empty set
for A1,A2 be non empty Subset of A
for f1 be Function of A1,B, f2 be Function of A2,B
st f1|(A1 /\ A2) = f2|(A1 /\ A2) holds
(f1 union f2)|A1 = f1 & (f1 union f2)|A2 = f2;