:: Topological Spaces and Continuous Functions
:: by Beata Padlewska and Agata Darmochwa\l
::
:: Copyright (c) 1990 Association of Mizar Users

begin

definition
attr c1 is strict ;
struct TopStruct -> 1-sorted ;
aggr TopStruct(# carrier, topology #) -> TopStruct ;
sel topology c1 -> Subset-Family of the carrier of c1;
end;

definition
let IT be TopStruct ;
attr IT is TopSpace-like means :Def1: :: PRE_TOPC:def 1
( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
a /\ b in the topology of IT ) );
end;

:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def 1 :
for IT being TopStruct holds
( IT is TopSpace-like iff ( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
a /\ b in the topology of IT ) ) );

registration
cluster non empty strict TopSpace-like TopStruct ;
existence
ex b1 being TopStruct st
( not b1 is empty & b1 is strict & b1 is TopSpace-like )
proof end;
end;

definition end;

definition
let S be 1-sorted ;
mode Point of S is Element of S;
end;

registration
let T be TopSpace;
cluster the topology of T -> non empty ;
coherence
not the topology of T is empty
by Def1;
end;

theorem :: PRE_TOPC:1
canceled;

theorem :: PRE_TOPC:2
canceled;

theorem :: PRE_TOPC:3
canceled;

theorem :: PRE_TOPC:4
canceled;

theorem Th5: :: PRE_TOPC:5
for GX being TopSpace holds {} in the topology of GX
proof end;

theorem :: PRE_TOPC:6
canceled;

theorem :: PRE_TOPC:7
canceled;

theorem :: PRE_TOPC:8
canceled;

theorem :: PRE_TOPC:9
canceled;

theorem :: PRE_TOPC:10
canceled;

theorem :: PRE_TOPC:11
canceled;

theorem :: PRE_TOPC:12
canceled;

theorem :: PRE_TOPC:13
canceled;

theorem :: PRE_TOPC:14
canceled;

theorem :: PRE_TOPC:15
canceled;

theorem :: PRE_TOPC:16
canceled;

theorem :: PRE_TOPC:17
canceled;

theorem :: PRE_TOPC:18
for T being 1-sorted
for P being Subset of T holds P \/ (P `) = [#] T
proof end;

theorem :: PRE_TOPC:19
canceled;

theorem :: PRE_TOPC:20
canceled;

theorem :: PRE_TOPC:21
canceled;

theorem Th22: :: PRE_TOPC:22
for T being 1-sorted
for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P
proof end;

theorem Th23: :: PRE_TOPC:23
for T being 1-sorted
for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )
proof end;

theorem :: PRE_TOPC:24
canceled;

theorem :: PRE_TOPC:25
for T being 1-sorted
for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P
proof end;

theorem :: PRE_TOPC:26
canceled;

theorem :: PRE_TOPC:27
for T being 1-sorted holds [#] T = ({} T) ` ;

definition
let T be TopStruct ;
let P be Subset of T;
canceled;
canceled;
canceled;
attr P is open means :Def5: :: PRE_TOPC:def 5
P in the topology of T;
end;

:: deftheorem PRE_TOPC:def 2 :
canceled;

:: deftheorem PRE_TOPC:def 3 :
canceled;

:: deftheorem PRE_TOPC:def 4 :
canceled;

:: deftheorem Def5 defines open PRE_TOPC:def 5 :
for T being TopStruct
for P being Subset of T holds
( P is open iff P in the topology of T );

definition
let T be TopStruct ;
let P be Subset of T;
attr P is closed means :Def6: :: PRE_TOPC:def 6
([#] T) \ P is open ;
end;

:: deftheorem Def6 defines closed PRE_TOPC:def 6 :
for T being TopStruct
for P being Subset of T holds
( P is closed iff ([#] T) \ P is open );

definition
canceled;
canceled;
let T be TopStruct ;
mode SubSpace of T -> TopStruct means :Def9: :: PRE_TOPC:def 9
( [#] it c= [#] T & ( for P being Subset of it holds
( P in the topology of it iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] it) ) ) ) );
existence
ex b1 being TopStruct st
( [#] b1 c= [#] T & ( for P being Subset of b1 holds
( P in the topology of b1 iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b1) ) ) ) )
proof end;
end;

:: deftheorem PRE_TOPC:def 7 :
canceled;

:: deftheorem PRE_TOPC:def 8 :
canceled;

:: deftheorem Def9 defines SubSpace PRE_TOPC:def 9 :
for T, b2 being TopStruct holds
( b2 is SubSpace of T iff ( [#] b2 c= [#] T & ( for P being Subset of b2 holds
( P in the topology of b2 iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b2) ) ) ) ) );

Lm1: for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
proof end;

registration
let T be TopStruct ;
cluster strict SubSpace of T;
existence
ex b1 being SubSpace of T st b1 is strict
proof end;
end;

registration
let T be non empty TopStruct ;
cluster non empty strict SubSpace of T;
existence
ex b1 being SubSpace of T st
( b1 is strict & not b1 is empty )
proof end;
end;

registration
let T be TopSpace;
cluster -> TopSpace-like SubSpace of T;
coherence
for b1 being SubSpace of T holds b1 is TopSpace-like
proof end;
end;

definition
let T be TopStruct ;
let P be Subset of T;
func T | P -> strict SubSpace of T means :Def10: :: PRE_TOPC:def 10
[#] it = P;
existence
ex b1 being strict SubSpace of T st [#] b1 = P
proof end;
uniqueness
for b1, b2 being strict SubSpace of T st [#] b1 = P & [#] b2 = P holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines | PRE_TOPC:def 10 :
for T being TopStruct
for P being Subset of T
for b3 being strict SubSpace of T holds
( b3 = T | P iff [#] b3 = P );

registration
let T be non empty TopStruct ;
let P be non empty Subset of T;
cluster T | P -> non empty strict ;
coherence
not T | P is empty
proof end;
end;

registration
let T be TopSpace;
cluster strict TopSpace-like SubSpace of T;
existence
ex b1 being SubSpace of T st
( b1 is TopSpace-like & b1 is strict )
proof end;
end;

registration
let T be TopSpace;
let P be Subset of T;
cluster T | P -> strict TopSpace-like ;
coherence
T | P is TopSpace-like
;
end;

theorem :: PRE_TOPC:28
for S being TopSpace
for P1, P2 being Subset of S
for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
proof end;

theorem Th29: :: PRE_TOPC:29
for GX being TopStruct
for A being Subset of GX holds the carrier of (GX | A) = A
proof end;

theorem :: PRE_TOPC:30
for X being TopStruct
for Y being non empty TopStruct
for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
proof end;

definition
let S, T be TopStruct ;
let f be Function of S,T;
canceled;
attr f is continuous means :Def12: :: PRE_TOPC:def 12
for P1 being Subset of T st P1 is closed holds
f " P1 is closed ;
end;

:: deftheorem PRE_TOPC:def 11 :
canceled;

:: deftheorem Def12 defines continuous PRE_TOPC:def 12 :
for S, T being TopStruct
for f being Function of S,T holds
( f is continuous iff for P1 being Subset of T st P1 is closed holds
f " P1 is closed );

theorem :: PRE_TOPC:31
for T1, T2, S1, S2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & S1 is SubSpace of T1 holds
S2 is SubSpace of T2
proof end;

theorem :: PRE_TOPC:32
canceled;

theorem :: PRE_TOPC:33
canceled;

theorem :: PRE_TOPC:34
canceled;

theorem :: PRE_TOPC:35
canceled;

theorem :: PRE_TOPC:36
canceled;

theorem :: PRE_TOPC:37
canceled;

theorem :: PRE_TOPC:38
canceled;

theorem Th39: :: PRE_TOPC:39
for T being TopStruct
for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T
proof end;

theorem :: PRE_TOPC:40
canceled;

theorem :: PRE_TOPC:41
for T being TopStruct
for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A
proof end;

registration
let T be TopSpace;
cluster [#] T -> closed ;
coherence
[#] T is closed
proof end;
end;

registration
let T be TopSpace;
cluster closed Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is closed
proof end;
end;

registration
let T be non empty TopSpace;
cluster non empty closed Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is closed )
proof end;
end;

theorem :: PRE_TOPC:42
canceled;

theorem Th43: :: PRE_TOPC:43
for T being TopStruct
for X9 being SubSpace of T
for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
proof end;

theorem Th44: :: PRE_TOPC:44
for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is closed ) holds
meet F is closed
proof end;

definition
let GX be TopStruct ;
let A be Subset of GX;
func Cl A -> Subset of GX means :Def13: :: PRE_TOPC:def 13
for p being set st p in the carrier of GX holds
( p in it iff for G being Subset of GX st G is open & p in G holds
A meets G );
existence
ex b1 being Subset of GX st
for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
A meets G )
proof end;
uniqueness
for b1, b2 being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) & ( for p being set st p in the carrier of GX holds
( p in b2 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) holds
b1 = b2
proof end;
projectivity
for b1, b2 being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
b2 meets G ) ) holds
for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
b1 meets G )
proof end;
end;

:: deftheorem Def13 defines Cl PRE_TOPC:def 13 :
for GX being TopStruct
for A, b3 being Subset of GX holds
( b3 = Cl A iff for p being set st p in the carrier of GX holds
( p in b3 iff for G being Subset of GX st G is open & p in G holds
A meets G ) );

theorem Th45: :: PRE_TOPC:45
for T being TopStruct
for A being Subset of T
for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
proof end;

theorem Th46: :: PRE_TOPC:46
for GX being TopSpace
for A being Subset of GX ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
proof end;

theorem :: PRE_TOPC:47
for T being TopStruct
for X9 being SubSpace of T
for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
proof end;

theorem Th48: :: PRE_TOPC:48
for T being TopStruct
for A being Subset of T holds A c= Cl A
proof end;

theorem Th49: :: PRE_TOPC:49
for T being TopStruct
for A, B being Subset of T st A c= B holds
Cl A c= Cl B
proof end;

theorem :: PRE_TOPC:50
for GX being TopSpace
for A, B being Subset of GX holds Cl (A \/ B) = (Cl A) \/ (Cl B)
proof end;

theorem :: PRE_TOPC:51
for T being TopStruct
for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ (Cl B)
proof end;

theorem Th52: :: PRE_TOPC:52
for T being TopStruct
for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
proof end;

theorem :: PRE_TOPC:53
for T being TopStruct
for A being Subset of T holds
( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
proof end;

theorem :: PRE_TOPC:54
for T being TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ( not T is empty & ( for G being Subset of T st G is open & p in G holds
A meets G ) ) ) by Def13;

begin

theorem :: PRE_TOPC:55
for T being non empty TopStruct
for A being non empty SubSpace of T
for p being Point of A holds p is Point of T
proof end;

theorem :: PRE_TOPC:56
for A, B, C being TopSpace
for f being Function of A,C st f is continuous & C is SubSpace of B holds
for h being Function of A,B st h = f holds
h is continuous
proof end;

theorem :: PRE_TOPC:57
for A being TopSpace
for B being non empty TopSpace
for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
proof end;

registration
let T be TopSpace;
cluster empty -> closed Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is empty holds
b1 is closed
proof end;
end;

registration
let X be TopSpace;
let Y be non empty TopSpace;
let y be Point of Y;
cluster X --> y -> continuous ;
coherence
X --> y is continuous
proof end;
end;

registration
let S be TopSpace;
let T be non empty TopSpace;
cluster V7() V10( the carrier of S) V11( the carrier of T) V12() V18( the carrier of S, the carrier of T) continuous Element of bool [: the carrier of S, the carrier of T:];
existence
ex b1 being Function of S,T st b1 is continuous
proof end;
end;

definition
let T be TopStruct ;
attr T is T_0 means :: PRE_TOPC:def 14
for x, y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y;
attr T is T_1 means :Def15: :: PRE_TOPC:def 15
for p, q being Point of T st p <> q holds
ex G being Subset of T st
( G is open & p in G & q in G ` );
attr T is T_2 means :Def16: :: PRE_TOPC:def 16
for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 );
attr T is regular means :: PRE_TOPC:def 17
for p being Point of T
for F being Subset of T st F is closed & p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 );
attr T is normal means :: PRE_TOPC:def 18
for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 );
end;

:: deftheorem defines T_0 PRE_TOPC:def 14 :
for T being TopStruct holds
( T is T_0 iff for x, y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y );

:: deftheorem Def15 defines T_1 PRE_TOPC:def 15 :
for T being TopStruct holds
( T is T_1 iff for p, q being Point of T st p <> q holds
ex G being Subset of T st
( G is open & p in G & q in G ` ) );

:: deftheorem Def16 defines T_2 PRE_TOPC:def 16 :
for T being TopStruct holds
( T is T_2 iff for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) );

:: deftheorem defines regular PRE_TOPC:def 17 :
for T being TopStruct holds
( T is regular iff for p being Point of T
for F being Subset of T st F is closed & p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 ) );

:: deftheorem defines normal PRE_TOPC:def 18 :
for T being TopStruct holds
( T is normal iff for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) );

definition
let T be TopStruct ;
attr T is T_3 means :Def19: :: PRE_TOPC:def 19
( T is T_1 & T is regular );
attr T is T_4 means :Def20: :: PRE_TOPC:def 20
( T is T_1 & T is normal );
end;

:: deftheorem Def19 defines T_3 PRE_TOPC:def 19 :
for T being TopStruct holds
( T is T_3 iff ( T is T_1 & T is regular ) );

:: deftheorem Def20 defines T_4 PRE_TOPC:def 20 :
for T being TopStruct holds
( T is T_4 iff ( T is T_1 & T is normal ) );

registration
cluster T_3 -> T_1 regular TopStruct ;
coherence
for b1 being TopStruct st b1 is T_3 holds
( b1 is T_1 & b1 is regular )
by Def19;
cluster T_1 regular -> T_3 TopStruct ;
coherence
for b1 being TopStruct st b1 is T_1 & b1 is regular holds
b1 is T_3
by Def19;
cluster T_4 -> T_1 normal TopStruct ;
coherence
for b1 being TopStruct st b1 is T_4 holds
( b1 is T_1 & b1 is normal )
by Def20;
cluster T_1 normal -> T_4 TopStruct ;
coherence
for b1 being TopStruct st b1 is T_1 & b1 is normal holds
b1 is T_4
by Def20;
end;

registration
cluster non empty TopSpace-like T_1 TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is T_1
proof end;
end;

registration
cluster T_1 -> T_0 TopStruct ;
coherence
for b1 being TopStruct st b1 is T_1 holds
b1 is T_0
proof end;
cluster T_2 -> T_1 TopStruct ;
coherence
for b1 being TopStruct st b1 is T_2 holds
b1 is T_1
proof end;
end;

registration
let T be TopSpace;
cluster TopStruct(# the carrier of T, the topology of T #) -> TopSpace-like ;
coherence
TopStruct(# the carrier of T, the topology of T #) is TopSpace-like
proof end;
end;

registration
let T be non empty TopStruct ;
cluster TopStruct(# the carrier of T, the topology of T #) -> non empty ;
coherence
not TopStruct(# the carrier of T, the topology of T #) is empty
;
end;

theorem :: PRE_TOPC:58
for T being TopStruct st TopStruct(# the carrier of T, the topology of T #) is TopSpace-like holds
T is TopSpace-like
proof end;

theorem :: PRE_TOPC:59
for T being TopStruct
for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T
proof end;

registration
let T be TopSpace;
cluster open Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is open
proof end;
end;

theorem :: PRE_TOPC:60
for T being TopSpace
for X being set holds
( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )
proof end;

theorem Th61: :: PRE_TOPC:61
for T being TopSpace
for X being set holds
( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )
proof end;

theorem Th62: :: PRE_TOPC:62
for S, T being TopSpace
for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds
( f is continuous iff g is continuous )
proof end;

theorem Th63: :: PRE_TOPC:63
for S, T being TopSpace
for f being Function of S,T
for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
proof end;

theorem :: PRE_TOPC:64
for S, T being TopSpace
for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
proof end;

registration
let T be TopStruct ;
let P be empty Subset of T;
cluster T | P -> empty strict ;
coherence
T | P is empty
by Th29;
end;

theorem Th65: :: PRE_TOPC:65
for S, T being TopStruct holds
( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )
proof end;

theorem :: PRE_TOPC:66
for T being TopStruct
for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
proof end;

registration
cluster empty strict TopStruct ;
existence
ex b1 being TopStruct st
( b1 is strict & b1 is empty )
proof end;
end;

registration
let A be non empty set ;
let t be Subset-Family of A;
cluster TopStruct(# A,t #) -> non empty ;
coherence
not TopStruct(# A,t #) is empty
;
end;