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

begin

definition

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

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 b₁ being TopStruct st
( not b₁ is empty & b₁ is strict & b₁ is TopSpace-like )

proof end;

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 :: 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 b₁ being TopStruct st
( [#] b₁ c= [#] T & ( for P being Subset of b₁ holds
( P in the topology of b₁ iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b₁) ) ) ) )

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, b₂ being TopStruct holds
( b₂ is SubSpace of T iff ( [#] b₂ c= [#] T & ( for P being Subset of b₂ holds
( P in the topology of b₂ iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b₂) ) ) ) ) );

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 b₁ being SubSpace of T st b₁ is strict

proof end;

end;

registration

let T be non empty TopStruct ;
cluster non empty strict SubSpace of T;
existence
ex b₁ being SubSpace of T st
( b₁ is strict & not b₁ is empty )

proof end;

end;

registration

let T be TopSpace;
cluster -> TopSpace-like SubSpace of T;
coherence
for b₁ being SubSpace of T holds b₁ 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 b₁ being strict SubSpace of T st [#] b₁ = P

proof end;

uniqueness
for b₁, b₂ being strict SubSpace of T st [#] b₁ = P & [#] b₂ = P holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines | PRE_TOPC:def 10 :
for T being TopStruct
for P being Subset of T
for b₃ being strict SubSpace of T holds
( b₃ = T | P iff [#] b₃ = 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 b₁ being SubSpace of T st
( b₁ is TopSpace-like & b₁ 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 b₁ being Subset of T st b₁ 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 b₁ being Subset of T st
( not b₁ is empty & b₁ 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 b₁ being Subset of GX st
for p being set st p in the carrier of GX holds
( p in b₁ iff for G being Subset of GX st G is open & p in G holds
A meets G )

proof end;

uniqueness
for b₁, b₂ being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b₁ 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 b₂ iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) holds
b₁ = b₂

proof end;

projectivity
for b₁, b₂ being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b₁ iff for G being Subset of GX st G is open & p in G holds
b₂ meets G ) ) holds
for p being set st p in the carrier of GX holds
( p in b₁ iff for G being Subset of GX st G is open & p in G holds
b₁ meets G )

proof end;

end;

:: deftheorem Def13 defines Cl PRE_TOPC:def 13 :
for GX being TopStruct
for A, b₃ being Subset of GX holds
( b₃ = Cl A iff for p being set st p in the carrier of GX holds
( p in b₃ 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 b₁ being Subset of T st b₁ is empty holds
b₁ 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 b₁ being Function of S,T st b₁ 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 b₁ being TopStruct st b₁ is T_3 holds
( b₁ is T_1 & b₁ is regular ) by Def19;
cluster T_1 regular -> T_3 TopStruct ;
coherence
for b₁ being TopStruct st b₁ is T_1 & b₁ is regular holds
b₁ is T_3 by Def19;
cluster T_4 -> T_1 normal TopStruct ;
coherence
for b₁ being TopStruct st b₁ is T_4 holds
( b₁ is T_1 & b₁ is normal ) by Def20;
cluster T_1 normal -> T_4 TopStruct ;
coherence
for b₁ being TopStruct st b₁ is T_1 & b₁ is normal holds
b₁ is T_4 by Def20;

end;

registration

cluster non empty TopSpace-like T_1 TopStruct ;
existence
ex b₁ being non empty TopSpace st b₁ is T_1

proof end;

end;

registration

cluster T_1 -> T_0 TopStruct ;
coherence
for b₁ being TopStruct st b₁ is T_1 holds
b₁ is T_0

proof end;

cluster T_2 -> T_1 TopStruct ;
coherence
for b₁ being TopStruct st b₁ is T_2 holds
b₁ 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 b₁ being Subset of T st b₁ 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 b₁ being TopStruct st
( b₁ is strict & b₁ 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;