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

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;

::
:: The topological space
::
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
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 Th1: :: PRE_TOPC:1
for GX being TopSpace holds {} in the topology of GX
proof end;

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

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

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

theorem :: PRE_TOPC:5
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:6
for T being 1-sorted holds [#] T = ({} T)  ;

definition
let T be TopStruct ;
let P be Subset of T;
attr P 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;
attr P 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 & ( 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 Def4 defines SubSpace PRE_TOPC:def 4 :
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 for 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 for 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 for 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 :Def5: :: PRE_TOPC:def 5
[#] 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 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;
cluster T | P -> non empty strict ;
coherence
not T | P is empty
proof end;
end;

registration
let T be TopSpace;
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;
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 & P1 c= P2 holds
S | P1 = (S | P2) | P19
proof end;

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

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
proof end;

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

:: deftheorem 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 #) & 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 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
proof end;

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
proof end;

registration
let T be TopSpace;
cluster [#] T -> closed ;
coherence
[#] T is closed
proof end;
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
proof end;
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 & b1 is closed )
proof end;
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 & C /\ ([#] X9) = B ) )
proof end;

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
proof end;

::
:: 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 & 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 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 & 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 & A c= C holds
p in C )
proof end;

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 & A c= C ) ) ) & Cl A = meet F )
proof end;

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)
proof end;

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

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
proof end;

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

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

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

:: 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
proof end;

theorem :: PRE_TOPC:26
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: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
proof end;

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
proof end;
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;
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() 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
proof end;
end;

:: from TSP_1, T_0TOPSP, COMPTS_1, URYSOHN1 2008.07.16, A.T.
definition
let T be TopStruct ;
attr T 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;
attr T is T_1 means :: 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 & p in G & q in G  );
attr T is T_2 means :: 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 & G2 is open & p in G1 & q in G2 & G1 misses G2 );
attr T is regular means :: PRE_TOPC:def 11
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 12
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 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 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 & p in G & q in G  ) );

:: deftheorem 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 & G2 is open & p in G1 & q in G2 & 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 & 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 12 :
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 :: PRE_TOPC:def 13
( T is T_1 & T is regular );
attr T is T_4 means :: PRE_TOPC:def 14
( T is T_1 & T is normal );
end;

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

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

registration
coherence
for b1 being TopStruct st b1 is T_3 holds
( b1 is T_1 & b1 is regular )
;
coherence
for b1 being TopStruct st b1 is T_1 & b1 is regular holds
b1 is T_3
;
coherence
for b1 being TopStruct st b1 is T_4 holds
( b1 is T_1 & b1 is normal )
;
coherence
for b1 being TopStruct st b1 is T_1 & b1 is normal holds
b1 is T_4
;
end;

registration
existence
ex b1 being non empty TopSpace st b1 is T_1
proof end;
end;

registration
cluster T_1 -> T_0 for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_1 holds
b1 is T_0
proof end;
cluster T_2 -> T_1 for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_2 holds
b1 is T_1
proof end;
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
by Def1;
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 ;

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
proof end;

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
proof end;
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 #) )
proof end;

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 #) )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

:: from BORSUK_3, 2009.03.15, A.T.
registration
let T be TopStruct ;
let P be empty Subset of T;
cluster T | 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 #) )
proof end;

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
proof end;

:: missing, 2009.05.26, A.T.
registration
existence
ex b1 being TopStruct st
( b1 is strict & b1 is empty )
proof end;
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
proof end;
end;

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