:: Basic Properties of Metrizable Topological Spaces
:: by Karol P\c{a}k
::
:: Received March 31, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

definition
let T1, T2 be TopSpace;
let A1 be Subset of T1;
let A2 be Subset of T2;
pred A1,A2 are_homeomorphic means :Def1: :: METRIZTS:def 1
T1 | A1,T2 | A2 are_homeomorphic ;
end;

:: deftheorem Def1 defines are_homeomorphic METRIZTS:def 1 :
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 holds
( A1,A2 are_homeomorphic iff T1 | A1,T2 | A2 are_homeomorphic );

Lm1: for T1, T2 being empty TopSpace holds T1,T2 are_homeomorphic
proof end;

theorem :: METRIZTS:1
for T1, T2 being TopSpace holds
( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic )
proof end;

theorem Th2: :: METRIZTS:2
for T1, T2 being TopSpace
for A1 being Subset of T1
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism
proof end;

theorem :: METRIZTS:3
for T1, T2 being TopSpace
for A1 being Subset of T1
for f being Function of T1,T2 st f is being_homeomorphism holds
A1,f .: A1 are_homeomorphic
proof end;

Lm2: for T1, T2 being non empty TopSpace st T1,T2 are_homeomorphic holds
weight T2 c= weight T1

proof end;

Lm3: for T being empty TopSpace holds weight T is empty
proof end;

theorem Th4: :: METRIZTS:4
for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
weight T1 = weight T2
proof end;

registration
cluster empty TopSpace-like -> metrizable for TopStruct ;
coherence
for b1 being TopSpace st b1 is empty holds
b1 is metrizable
proof end;
cluster TopSpace-like metrizable -> T_4 for TopStruct ;
coherence
for b1 being TopSpace st b1 is metrizable holds
b1 is T_4
proof end;
let M be MetrSpace;
cluster TopSpaceMetr M -> metrizable ;
coherence
TopSpaceMetr M is metrizable
proof end;
end;

registration
let TM be metrizable TopSpace;
let Am be Subset of TM;
cluster TM | Am -> metrizable ;
coherence
TM | Am is metrizable
proof end;
end;

registration
let TM1, TM2 be metrizable TopSpace;
cluster [:TM1,TM2:] -> metrizable ;
coherence
[:TM1,TM2:] is metrizable
proof end;
end;

registration
let T be empty TopSpace;
cluster weight T -> empty ;
coherence
weight T is empty
by Lm3;
end;

theorem Th5: :: METRIZTS:5
for T1, T2 being TopSpace holds weight [:T1,T2:] c= (weight T1) *` (weight T2)
proof end;

theorem Th6: :: METRIZTS:6
for T1, T2 being TopSpace st not T1 is empty & not T2 is empty holds
( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] )
proof end;

registration
let T1, T2 be second-countable TopSpace;
cluster [:T1,T2:] -> second-countable ;
coherence
[:T1,T2:] is second-countable
proof end;
end;

theorem Th7: :: METRIZTS:7
for T being TopSpace
for A being Subset of T
for F being Subset-Family of T holds card (F | A) c= card F
proof end;

theorem Th8: :: METRIZTS:8
for T being TopSpace
for A being Subset of T
for Bas being Basis of T holds Bas | A is Basis of (T | A)
proof end;

registration
let T be second-countable TopSpace;
let A be Subset of T;
cluster T | A -> second-countable ;
coherence
T | A is second-countable
proof end;
end;

registration
let M be non empty MetrSpace;
let A be non empty Subset of (TopSpaceMetr M);
cluster dist_min A -> continuous ;
coherence
dist_min A is continuous
proof end;
end;

theorem :: METRIZTS:9
for T being TopSpace
for A, B being Subset of T
for F being Subset of (T | A) st F = B holds
(T | A) | F = T | B
proof end;

Lm4: for M being non empty MetrSpace
for A being non empty Subset of (TopSpaceMetr M)
for r being real number holds { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M)

proof end;

:: F_sigma and G_delta Types of Subsets
registration
let TM be metrizable TopSpace;
cluster open -> F_sigma for Element of bool the carrier of TM;
coherence
for b1 being Subset of TM st b1 is open holds
b1 is F_sigma
proof end;
cluster closed -> G_delta for Element of bool the carrier of TM;
coherence
for b1 being Subset of TM st b1 is closed holds
b1 is G_delta
proof end;
end;

theorem :: METRIZTS:10
for T being TopSpace
for B, A being Subset of T
for F being Subset of (T | B) st A is F_sigma & F = A /\ B holds
F is F_sigma
proof end;

theorem :: METRIZTS:11
for T being TopSpace
for B, A being Subset of T
for F being Subset of (T | B) st A is G_delta & F = A /\ B holds
F is G_delta
proof end;

theorem Th12: :: METRIZTS:12
for T being TopSpace
for A being Subset of T st T is T_1 & A is discrete holds
A is open Subset of (T | (Cl A))
proof end;

Lm5: for iC being infinite Cardinal holds omega *` iC = iC
proof end;

theorem Th13: :: METRIZTS:13
for C being Cardinal
for T being TopSpace st ( for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= C ) ) holds
for A being Subset of T st A is closed & A is discrete holds
card A c= C
proof end;

theorem Th14: :: METRIZTS:14
for iC being infinite Cardinal
for TM being metrizable TopSpace st ( for Am being Subset of TM st Am is closed & Am is discrete holds
card Am c= iC ) holds
for Am being Subset of TM st Am is discrete holds
card Am c= iC
proof end;

theorem Th15: :: METRIZTS:15
for C being Cardinal
for T being TopSpace st ( for A being Subset of T st A is discrete holds
card A c= C ) holds
for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) holds
card F c= C
proof end;

theorem Th16: :: METRIZTS:16
for T being TopSpace
for F being Subset-Family of T st F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= card ([#] T) )
proof end;

Lm6: for TM being metrizable TopSpace
for iC being infinite Cardinal st ( for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds
Am misses Bm ) holds
card Fm c= iC ) holds
density TM c= iC

proof end;

theorem Th17: :: METRIZTS:17
for TM being metrizable TopSpace
for Am being Subset of TM st Am is dense holds
weight TM c= omega *` (card Am)
proof end;

Lm7: for TM being metrizable TopSpace
for iC being infinite Cardinal st density TM c= iC holds
weight TM c= iC

proof end;

begin

:: General Topology Th 4.1.15 (a) <=> (c)
theorem Th18: :: METRIZTS:18
for TM being metrizable TopSpace
for iC being infinite Cardinal holds
( weight TM c= iC iff for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds
ex Gm being Subset-Family of TM st
( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) )
proof end;

:: General Topology Th 4.1.15 (a) <=> (d)
theorem Th19: :: METRIZTS:19
for TM being metrizable TopSpace
for iC being infinite Cardinal holds
( weight TM c= iC iff for Am being Subset of TM st Am is closed & Am is discrete holds
card Am c= iC )
proof end;

:: General Topology Th 4.1.15 (a) <=> (e)
theorem Th20: :: METRIZTS:20
for TM being metrizable TopSpace
for iC being infinite Cardinal holds
( weight TM c= iC iff for Am being Subset of TM st Am is discrete holds
card Am c= iC )
proof end;

:: General Topology Th 4.1.15 (a) <=> (f)
theorem Th21: :: METRIZTS:21
for TM being metrizable TopSpace
for iC being infinite Cardinal holds
( weight TM c= iC iff for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds
Am misses Bm ) holds
card Fm c= iC )
proof end;

:: General Topology Th 4.1.15 (a) <=> (g)
theorem Th22: :: METRIZTS:22
for TM being metrizable TopSpace
for iC being infinite Cardinal holds
( weight TM c= iC iff density TM c= iC )
proof end;

theorem Th23: :: METRIZTS:23
for TM being metrizable TopSpace
for iC being infinite Cardinal
for B being Basis of TM st ( for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds
ex Gm being Subset-Family of TM st
( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) ) holds
ex underB being Basis of TM st
( underB c= B & card underB c= iC )
proof end;

begin

definition
let T be TopSpace;
attr T is Lindelof means :Def2: :: METRIZTS:def 2
for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable );
end;

:: deftheorem Def2 defines Lindelof METRIZTS:def 2 :
for T being TopSpace holds
( T is Lindelof iff for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable ) );

Lm8: for T being TopSpace holds
( T is Lindelof iff for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= omega ) )

proof end;

theorem :: METRIZTS:24
for TM being metrizable TopSpace
for B being Basis of TM st TM is Lindelof holds
ex B9 being Basis of TM st
( B9 c= B & B9 is countable )
proof end;

Lm9: for TM being metrizable TopSpace holds
( TM is Lindelof iff TM is second-countable )

proof end;

registration
cluster TopSpace-like metrizable Lindelof -> second-countable metrizable for TopStruct ;
coherence
for b1 being metrizable TopSpace st b1 is Lindelof holds
b1 is second-countable
by Lm9;
end;

Lm10: for TM being metrizable TopSpace holds
( TM is Lindelof iff TM is separable )

proof end;

registration
cluster TopSpace-like metrizable Lindelof -> separable metrizable for TopStruct ;
coherence
for b1 being metrizable TopSpace st b1 is Lindelof holds
b1 is separable
by Lm10;
cluster TopSpace-like separable metrizable -> metrizable Lindelof for TopStruct ;
coherence
for b1 being metrizable TopSpace st b1 is separable holds
b1 is Lindelof
by Lm10;
end;

registration
cluster non empty TopSpace-like metrizable Lindelof for TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is Lindelof & b1 is metrizable )
proof end;
cluster TopSpace-like second-countable -> Lindelof for TopStruct ;
coherence
for b1 being TopSpace st b1 is second-countable holds
b1 is Lindelof
proof end;
cluster TopSpace-like regular Lindelof -> normal for TopStruct ;
coherence
for b1 being TopSpace st b1 is regular & b1 is Lindelof holds
b1 is normal
proof end;
cluster TopSpace-like countable -> Lindelof for TopStruct ;
coherence
for b1 being TopSpace st b1 is countable holds
b1 is Lindelof
proof end;
end;

Lm11: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is second-countable
proof end;

registration
let n be Nat;
cluster TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) -> second-countable ;
coherence
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is second-countable
proof end;
end;

registration
let T be Lindelof TopSpace;
let A be closed Subset of T;
cluster T | A -> Lindelof ;
coherence
T | A is Lindelof
proof end;
end;

registration
let TM be metrizable Lindelof TopSpace;
let A be Subset of TM;
cluster TM | A -> Lindelof ;
coherence
TM | A is Lindelof
;
end;

definition
let T be TopSpace;
let A, B, L be Subset of T;
pred L separates A,B means :Def3: :: METRIZTS:def 3
ex U, W being open Subset of T st
( A c= U & B c= W & U misses W & L = (U \/ W) ` );
end;

:: deftheorem Def3 defines separates METRIZTS:def 3 :
for T being TopSpace
for A, B, L being Subset of T holds
( L separates A,B iff ex U, W being open Subset of T st
( A c= U & B c= W & U misses W & L = (U \/ W) ` ) );

Lm12: for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) holds { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } is open Subset of (TopSpaceMetr M)

proof end;

Lm13: for TM being metrizable TopSpace
for A, B being Subset of TM st A,B are_separated holds
ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )

proof end;

:: Teoria wymiaru Lm 1.2.8
theorem :: METRIZTS:25
for TM being metrizable TopSpace
for Am, Bm being Subset of TM st Am,Bm are_separated holds
ex L being Subset of TM st L separates Am,Bm
proof end;

:: Teoria wymiaru Lm 1.2.9
theorem :: METRIZTS:26
for TM being metrizable TopSpace
for M being Subset of TM
for A1, A2 being closed Subset of TM
for V1, V2 being open Subset of TM st A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 holds
for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds
ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL )
proof end;