:: Basic Properties of Metrizable Topological Spaces
:: by Karol P\c{a}k
::
:: Received March 31, 2009
:: Copyright (c) 2009-2011 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 TopStruct ;
coherence
for b₁ being TopSpace st b₁ is empty holds
b₁ is metrizable

proof end;

cluster TopSpace-like metrizable -> T_4 TopStruct ;
coherence
for b₁ being TopSpace st b₁ is metrizable holds
b₁ 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;

registration

let TM be metrizable TopSpace;
cluster open -> F_sigma Element of bool the carrier of TM;
coherence
for b₁ being Subset of TM st b₁ is open holds
b₁ is F_sigma

proof end;

cluster closed -> G_delta Element of bool the carrier of TM;
coherence
for b₁ being Subset of TM st b₁ is closed holds
b₁ 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

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;

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;

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;

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;

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 TopStruct ;
coherence
for b₁ being metrizable TopSpace st b₁ is Lindelof holds
b₁ 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 TopStruct ;
coherence
for b₁ being metrizable TopSpace st b₁ is Lindelof holds
b₁ is separable by Lm10;
cluster TopSpace-like separable metrizable -> metrizable Lindelof TopStruct ;
coherence
for b₁ being metrizable TopSpace st b₁ is separable holds
b₁ is Lindelof by Lm10;

end;

registration

cluster non empty TopSpace-like metrizable Lindelof TopStruct ;
existence
ex b₁ being non empty TopSpace st
( b₁ is Lindelof & b₁ is metrizable )

proof end;

cluster TopSpace-like second-countable -> Lindelof TopStruct ;
coherence
for b₁ being TopSpace st b₁ is second-countable holds
b₁ is Lindelof

proof end;

cluster TopSpace-like regular Lindelof -> normal TopStruct ;
coherence
for b₁ being TopSpace st b₁ is regular & b₁ is Lindelof holds
b₁ is normal

proof end;

cluster TopSpace-like countable -> Lindelof TopStruct ;
coherence
for b₁ being TopSpace st b₁ is countable holds
b₁ 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;

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;

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;