:: Compact Spaces
:: by Agata Darmochwa{\l}
::
:: Received September 19, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let T be TopStruct ;

attr T is compact means :: COMPTS_1:def 1
for F being Subset-Family of T st F is Cover of T & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite );

end;

:: deftheorem defines compact COMPTS_1:def 1 :
for T being TopStruct holds
( T is compact iff for F being Subset-Family of T st F is Cover of T & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) );

definition

let T be non empty TopSpace;

redefine attr T is regular means :: COMPTS_1:def 2
for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V );

compatibility
( T is regular iff for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) )

proof end;

redefine attr T is normal means :: COMPTS_1:def 3
for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q );

compatibility
( T is normal iff for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) )

proof end;

end;

:: deftheorem defines regular COMPTS_1:def 2 :
for T being non empty TopSpace holds
( T is regular iff for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) );

:: deftheorem defines normal COMPTS_1:def 3 :
for T being non empty TopSpace holds
( T is normal iff for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) );

notation

let T be TopStruct ;
synonym Hausdorff T for T_2 ;

end;

definition

let T be TopStruct ;
let P be Subset of T;

attr P is compact means :Def4: :: COMPTS_1:def 4
for F being Subset-Family of T st F is Cover of P & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite );

end;

:: deftheorem Def4 defines compact COMPTS_1:def 4 :
for T being TopStruct
for P being Subset of T holds
( P is compact iff for F being Subset-Family of T st F is Cover of P & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite ) );

registration

let T be TopStruct ;

cluster empty -> compact for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is empty holds
b₁ is compact

proof end;

end;

theorem :: COMPTS_1:1

for T being TopStruct holds
( T is compact iff [#] T is compact ) ;

theorem Th2: :: COMPTS_1:2

for T being TopStruct
for A being SubSpace of T
for Q being Subset of T st Q c= [#] A holds
( Q is compact iff for P being Subset of A st P = Q holds
P is compact )

proof end;

theorem Th3: :: COMPTS_1:3

for T being TopStruct
for P being Subset of T holds
( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) )

proof end;

theorem Th4: :: COMPTS_1:4

for T being non empty TopSpace holds
( T is compact iff for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} )

proof end;

theorem :: COMPTS_1:5

for T being non empty TopSpace holds
( T is compact iff for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) )

proof end;

theorem Th6: :: COMPTS_1:6

for TS being TopSpace st TS is T_2 holds
for A being Subset of TS st A <> {} & A is compact holds
for p being Point of TS st p in A ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & A c= QS & PS misses QS )

proof end;

theorem Th7: :: COMPTS_1:7

for TS being TopSpace
for PS being Subset of TS st TS is T_2 & PS is compact holds
PS is closed

proof end;

theorem Th8: :: COMPTS_1:8

for T being TopStruct
for P being Subset of T st T is compact & P is closed holds
P is compact

proof end;

theorem Th9: :: COMPTS_1:9

for TS being TopSpace
for PS, QS being Subset of TS st PS is compact & QS c= PS & QS is closed holds
QS is compact

proof end;

theorem :: COMPTS_1:10

for T being TopStruct
for P, Q being Subset of T st P is compact & Q is compact holds
P \/ Q is compact

proof end;

theorem :: COMPTS_1:11

for TS being TopSpace
for PS, QS being Subset of TS st TS is T_2 & PS is compact & QS is compact holds
PS /\ QS is compact

proof end;

theorem :: COMPTS_1:12

for TS being non empty TopSpace st TS is T_2 & TS is compact holds
TS is regular by Th6, Th8;

theorem :: COMPTS_1:13

for TS being non empty TopSpace st TS is T_2 & TS is compact holds
TS is normal

proof end;

theorem :: COMPTS_1:14

for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds
S is compact

proof end;

theorem Th15: :: COMPTS_1:15

for T being TopStruct
for P being Subset of T
for S being non empty TopStruct
for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds
f .: P is compact

proof end;

theorem Th16: :: COMPTS_1:16

for TS being TopSpace
for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds
for PS being Subset of TS st PS is closed holds
f .: PS is closed

proof end;

theorem :: COMPTS_1:17

for TS being TopSpace
for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is one-to-one & f is continuous holds
f is being_homeomorphism

proof end;

definition

let D be set ;

func 1TopSp D -> TopStruct equals :: COMPTS_1:def 5
TopStruct(# D,([#] (bool D)) #);

coherence
TopStruct(# D,([#] (bool D)) #) is TopStruct ;

end;

:: deftheorem defines 1TopSp COMPTS_1:def 5 :
for D being set holds 1TopSp D = TopStruct(# D,([#] (bool D)) #);

registration

let D be set ;

cluster 1TopSp D -> strict TopSpace-like ;

coherence
( 1TopSp D is strict & 1TopSp D is TopSpace-like ) by ZFMISC_1:def 1;

end;

registration

let D be non empty set ;

cluster 1TopSp D -> non empty ;

coherence
not 1TopSp D is empty ;

end;

registration

let x be set ;

cluster 1TopSp {x} -> T_2 ;

coherence
1TopSp {x} is Hausdorff

proof end;

end;

registration

cluster non empty TopSpace-like T_2 for TopStruct ;

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

proof end;

end;

registration

let T be non empty T_2 TopSpace;

cluster compact -> closed for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is compact holds
b₁ is closed by Th7;

end;

registration

let A be finite set ;

cluster 1TopSp A -> finite ;

coherence
1TopSp A is finite ;

end;

registration

cluster non empty finite strict TopSpace-like for TopStruct ;

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

proof end;

end;

registration

cluster finite TopSpace-like -> compact for TopStruct ;

coherence
for b₁ being TopSpace st b₁ is finite holds
b₁ is compact ;

end;

theorem :: COMPTS_1:18

for T being TopSpace st the carrier of T is finite holds
T is compact ;

registration

let T be TopSpace;

cluster finite -> compact for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is finite holds
b₁ is compact

proof end;

end;

registration

let T be non empty TopSpace;

cluster non empty compact for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st
( not b₁ is empty & b₁ is compact )

proof end;

end;

:: comp. TOPMETR:3, 2008.07.06, A.T.

registration

cluster empty -> T_2 for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is empty holds
b₁ is T_2 by STRUCT_0:def 10;

end;

registration

let T be T_2 TopStruct ;

cluster -> T_2 for SubSpace of T;

coherence
for b₁ being SubSpace of T holds b₁ is T_2

proof end;

end;

:: from BORSUK_1, 2008.07.07, A.T.

theorem Th19: :: COMPTS_1:19

for X being TopStruct
for Y being SubSpace of X
for A being Subset of X
for B being Subset of Y st A = B holds
( A is compact iff B is compact )

proof end;

Lm1: for T, S being non empty TopSpace
for X being set
for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X holds
f +* g is continuous Function of T,S

proof end;

theorem :: COMPTS_1:20

for T, S being non empty TopSpace
for p being Point of T
for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds
f +* g is continuous Function of T,S

proof end;

theorem :: COMPTS_1:21

for S, T being non empty TopSpace
for T1, T2 being SubSpace of T
for p1, p2 being Point of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S

proof end;

registration

let S be TopStruct ;

cluster the topology of S -> open ;

coherence
the topology of S is open

proof end;

end;

:: TOPGEN_2, A.T. 2009.03.15

registration

let T be TopSpace;

cluster non empty open for Element of bool (bool the carrier of T);

existence
ex b₁ being Subset-Family of T st
( b₁ is open & not b₁ is empty )

proof end;

end;

theorem Th22: :: COMPTS_1:22

for T being non empty TopSpace
for F being set holds
( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) )

proof end;

theorem :: COMPTS_1:23

for T being non empty TopSpace
for X being set holds
( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) )

proof end;

theorem :: COMPTS_1:24

for T, S being non empty TopSpace
for X being set
for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X holds
f +* g is continuous Function of T,S by Lm1;