:: Topological Spaces and Continuous Functions
:: by Beata Padlewska and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

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

::
:: The topological space
::
definition
let IT be TopStruct ;
attrIT 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 for TopStruct ;
existence
 ex b1 being TopStruct st
( not b1 is empty & b1 is strict & b1 is TopSpace-like )
proofend;
end;

definition
mode TopSpace is TopSpace-like TopStruct ;
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 Th1: :: PRE_TOPC:1
for GX being TopSpace holds {} in the topology of GX
proofend;

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

theorem Th3: :: PRE_TOPC:3
for T being 1-sorted
for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P
proofend;

theorem Th4: :: PRE_TOPC:4
for T being 1-sorted
for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )
proofend;

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

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

definition
let T be TopStruct ;
let P be Subset of T;
attrP is open  means :Def2: :: PRE_TOPC:def 2
P in the topology of T;
end;

:: deftheorem Def2 defines open PRE_TOPC:def_2_:_
 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;
attrP is closed  means :Def3: :: PRE_TOPC:def 3
([#] T) \ P is open ;
end;

:: deftheorem Def3 defines closed PRE_TOPC:def_3_:_
 for T being TopStruct
for P being Subset of T holds
( P is closed iff ([#] T) \ P is open );

definition
let T be TopStruct ;
mode SubSpace of T ->  TopStruct  means :Def4: :: PRE_TOPC:def 4
( [#] it c= [#] T &amp; ( 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 &amp; P = Q /\ ([#] it) ) ) ) );
existence
 ex b1 being TopStruct st
( [#] b1 c= [#] T &amp; ( 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 &amp; P = Q /\ ([#] b1) ) ) ) )
proofend;
end;

:: deftheorem Def4 defines SubSpace PRE_TOPC:def_4_:_
 for T, b2 being TopStruct holds
( b2 is SubSpace of T iff ( [#] b2 c= [#] T &amp; ( 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 &amp; P = Q /\ ([#] b2) ) ) ) ) );

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

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

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

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

definition
let T be TopStruct ;
let P be Subset of T;
funcT | P ->  strict SubSpace of T means :Def5: :: PRE_TOPC:def 5
 [#] it = P;
existence
 ex b1 being strict SubSpace of T st [#] b1 = P
proofend;
uniqueness
 for b1, b2 being strict SubSpace of T st [#] b1 = P &amp; [#] b2 = P holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines | PRE_TOPC:def_5_:_
 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;
clusterT | P ->  non empty strict ;
coherence
 not T | P is empty
proofend;
end;

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

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

theorem :: PRE_TOPC:7
for S being TopSpace
for P1, P2 being Subset of S
for P19 being Subset of (S | P2) st P1 = P19 &amp; P1 c= P2 holds
S | P1 = (S | P2) | P19
proofend;

theorem Th8: :: PRE_TOPC:8
for GX being TopStruct
for A being Subset of GX holds the carrier of (GX | A) = A
proofend;

theorem :: PRE_TOPC:9
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
proofend;

definition
let S, T be TopStruct ;
let f be Function of S,T;
attrf is continuous  means :Def6: :: PRE_TOPC:def 6
 for P1 being Subset of T st P1 is closed holds
f " P1 is closed ;
end;

:: deftheorem Def6 defines continuous PRE_TOPC:def_6_:_
 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:10
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 #) &amp; TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) &amp; S1 is SubSpace of T1 holds
S2 is SubSpace of T2
proofend;

theorem Th11: :: PRE_TOPC:11
for T being TopStruct
for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T
proofend;

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

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

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

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

theorem Th13: :: PRE_TOPC:13
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 &amp; C /\ ([#] X9) = B ) )
proofend;

theorem Th14: :: PRE_TOPC:14
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
proofend;

::
:: The closure of a set
::
definition
let GX be TopStruct ;
let A be Subset of GX;
func Cl A ->  Subset of GX means :Def7: :: PRE_TOPC:def 7
 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 &amp; 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 &amp; p in G holds
A meets G )
proofend;
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 &amp; p in G holds
A meets G ) ) &amp; ( 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 &amp; p in G holds
A meets G ) ) holds
b1 = b2
proofend;
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 &amp; 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 &amp; p in G holds
b1 meets G )
proofend;
end;

:: deftheorem Def7 defines Cl PRE_TOPC:def_7_:_
 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 &amp; p in G holds
A meets G ) );

theorem Th15: :: PRE_TOPC:15
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 &amp; A c= C holds
p in C )
proofend;

theorem Th16: :: PRE_TOPC:16
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 &amp; A c= C ) ) ) &amp; Cl A = meet F )
proofend;

theorem :: PRE_TOPC:17
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)
proofend;

theorem Th18: :: PRE_TOPC:18
for T being TopStruct
for A being Subset of T holds A c= Cl A
proofend;

theorem Th19: :: PRE_TOPC:19
for T being TopStruct
for A, B being Subset of T st A c= B holds
Cl A c= Cl B
proofend;

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

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

theorem Th22: :: PRE_TOPC:22
for T being TopStruct
for A being Subset of T holds
( ( A is closed implies Cl A = A ) &amp; ( T is TopSpace-like &amp; Cl A = A implies A is closed ) )
proofend;

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

theorem :: PRE_TOPC:24
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 &amp; ( for G being Subset of T st G is open &amp; p in G holds
A meets G ) ) ) by Def7;

begin

:: from TOPMETR, 2008.07.06, A.T.
theorem :: PRE_TOPC:25
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
proofend;

theorem :: PRE_TOPC:26
for A, B, C being TopSpace
for f being Function of A,C st f is continuous &amp; C is SubSpace of B holds
for h being Function of A,B st h = f holds
h is continuous
proofend;

theorem :: PRE_TOPC:27
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
proofend;

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

:: from BORSUK_1, 2008.07.07, A.T.
registration
let X be TopSpace;
let Y be non empty TopStruct ;
let y be Point of Y;
clusterX --> y ->  continuous ;
coherence
 X --> y is continuous
proofend;
end;

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

:: from TSP_1, T_0TOPSP, COMPTS_1, URYSOHN1 2008.07.16, A.T.
definition
let T be TopStruct ;
attrT is T_0  means :: PRE_TOPC:def 8
 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;
attrT is T_1  means :Def9: :: PRE_TOPC:def 9
 for p, q being Point of T st p <> q holds
ex G being Subset of T st
( G is open &amp; p in G &amp; q in G ` );
attrT is T_2  means :Def10: :: PRE_TOPC:def 10
 for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open &amp; G2 is open &amp; p in G1 &amp; q in G2 &amp; G1 misses G2 );
attrT is regular  means :: PRE_TOPC:def 11
 for p being Point of T
for F being Subset of T st F is closed &amp; p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open &amp; G2 is open &amp; p in G1 &amp; F c= G2 &amp; G1 misses G2 );
attrT is normal  means :: PRE_TOPC:def 12
 for F1, F2 being Subset of T st F1 is closed &amp; F2 is closed &amp; F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open &amp; G2 is open &amp; F1 c= G1 &amp; F2 c= G2 &amp; G1 misses G2 );
end;

:: deftheorem  defines T_0 PRE_TOPC:def_8_:_
 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 Def9 defines T_1 PRE_TOPC:def_9_:_
 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 &amp; p in G &amp; q in G ` ) );

:: deftheorem Def10 defines T_2 PRE_TOPC:def_10_:_
 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 &amp; G2 is open &amp; p in G1 &amp; q in G2 &amp; G1 misses G2 ) );

:: deftheorem  defines regular PRE_TOPC:def_11_:_
 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 &amp; p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open &amp; G2 is open &amp; p in G1 &amp; F c= G2 &amp; G1 misses G2 ) );

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

definition
let T be TopStruct ;
attrT is T_3  means :Def13: :: PRE_TOPC:def 13
( T is T_1 &amp; T is regular );
attrT is T_4  means :Def14: :: PRE_TOPC:def 14
( T is T_1 &amp; T is normal );
end;

:: deftheorem Def13 defines T_3 PRE_TOPC:def_13_:_
 for T being TopStruct holds
( T is T_3 iff ( T is T_1 &amp; T is regular ) );

:: deftheorem Def14 defines T_4 PRE_TOPC:def_14_:_
 for T being TopStruct holds
( T is T_4 iff ( T is T_1 &amp; T is normal ) );

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

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

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

:: missing, 2009.02.14, A.T.
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
proofend;
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:28
for T being TopStruct st TopStruct(# the carrier of T, the topology of T #) is TopSpace-like holds
T is TopSpace-like
proofend;

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

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

theorem :: PRE_TOPC:30
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 #) )
proofend;

theorem Th31: :: PRE_TOPC:31
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 #) )
proofend;

theorem Th32: :: PRE_TOPC:32
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 )
proofend;

theorem Th33: :: PRE_TOPC:33
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 )
proofend;

theorem :: PRE_TOPC:34
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 )
proofend;

:: from BORSUK_3, 2009.03.15, A.T.
registration
let T be TopStruct ;
let P be empty Subset of T;
clusterT | P ->  empty strict ;
coherence
 T | P is empty by Th8;
end;

theorem Th35: :: PRE_TOPC:35
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 #) )
proofend;

theorem :: PRE_TOPC:36
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
proofend;

:: missing, 2009.05.26, A.T.
registration
cluster empty strict for TopStruct ;
existence
 ex b1 being TopStruct st
( b1 is strict &amp; b1 is empty )
proofend;
end;

:: from COMPLSP1, 2010.02.25, A.T.
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;

:: from BORSUK_3, 2011.07.08. A.T.
registration
cluster empty  ->  T_0 for TopStruct ;
coherence
 for b1 being TopStruct st b1 is empty holds
b1 is T_0
proofend;
end;

registration
cluster empty strict TopSpace-like for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is strict &amp; b1 is empty )
proofend;
end;