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

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;

::
:: 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

cluster non empty strict TopSpace-like for 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 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 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 Def4 defines SubSpace PRE_TOPC:def 4 :
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 for 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 for 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 for 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 :Def5: :: PRE_TOPC:def 5
[#] 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 Def5 defines | PRE_TOPC:def 5 :
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 for 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: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 b₁ being Subset of T st b₁ 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 b₁ being Subset of T st
( not b₁ is empty & b₁ 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 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 Def7 defines Cl PRE_TOPC:def 7 :
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 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 b₁ being Subset of T st b₁ is empty holds
b₁ 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 b₁ being Function of S,T st b₁ 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

cluster T_3 -> T_1 regular for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is T_3 holds
( b₁ is T_1 & b₁ is regular ) ;

cluster T_1 regular -> T_3 for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is T_1 & b₁ is regular holds
b₁ is T_3 ;

cluster T_4 -> T_1 normal for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is T_4 holds
( b₁ is T_1 & b₁ is normal ) ;

cluster T_1 normal -> T_4 for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is T_1 & b₁ is normal holds
b₁ is T_4 ;

end;

registration

cluster non empty TopSpace-like T_1 for TopStruct ;

existence
ex b₁ being non empty TopSpace st b₁ is T_1

proof end;

end;

registration

cluster T_1 -> T_0 for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is T_1 holds
b₁ is T_0

proof end;

cluster T_2 -> T_1 for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is T_2 holds
b₁ 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 b₁ being Subset of T st b₁ 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

cluster empty strict for TopStruct ;

existence
ex b₁ being TopStruct st
( b₁ is strict & b₁ 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 b₁ being TopStruct st b₁ is empty holds
b₁ is T_0

proof end;

end;

registration

cluster empty strict TopSpace-like for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is strict & b₁ is empty )

proof end;

end;