:: 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; predA1,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 proofend; theorem :: METRIZTS:1 for T1, T2 being TopSpace holds ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic ) proofend; 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 proofend; 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 proofend; Lm2: for T1, T2 being non empty TopSpace st T1,T2 are_homeomorphic holds weight T2 c= weight T1 proofend; Lm3: for T being empty TopSpace holds weight T is empty proofend; theorem Th4: :: METRIZTS:4 for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds weight T1 = weight T2 proofend; registration cluster empty TopSpace-like -> metrizable for TopStruct ; coherence for b1 being TopSpace st b1 is empty holds b1 is metrizable proofend; cluster TopSpace-like metrizable -> T_4 for TopStruct ; coherence for b1 being TopSpace st b1 is metrizable holds b1 is T_4 proofend; let M be MetrSpace; cluster TopSpaceMetr M -> metrizable ; coherence TopSpaceMetr M is metrizable proofend; end; registration let TM be metrizable TopSpace; let Am be Subset of TM; clusterTM | Am -> metrizable ; coherence TM | Am is metrizable proofend; end; registration let TM1, TM2 be metrizable TopSpace; cluster[:TM1,TM2:] -> metrizable ; coherence [:TM1,TM2:] is metrizable proofend; 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) proofend; 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:] ) proofend; registration let T1, T2 be second-countable TopSpace; cluster[:T1,T2:] -> second-countable ; coherence [:T1,T2:] is second-countable proofend; 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 proofend; 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) proofend; registration let T be second-countable TopSpace; let A be Subset of T; clusterT | A -> second-countable ; coherence T | A is second-countable proofend; 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 proofend; 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 proofend; 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) proofend; :: 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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)) proofend; Lm5: for iC being infinite Cardinal holds omega *` iC = iC proofend; 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 proofend; 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 proofend; 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 proofend; 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) ) proofend; 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 proofend; 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) proofend; Lm7: for TM being metrizable TopSpace for iC being infinite Cardinal st density TM c= iC holds weight TM c= iC proofend; 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 ) ) proofend; :: 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 ) proofend; :: 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 ) proofend; :: 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 ) proofend; :: 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 ) proofend; 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 ) proofend; begin definition let T be TopSpace; attrT 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 ) ) proofend; 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 ) proofend; Lm9: for TM being metrizable TopSpace holds ( TM is Lindelof iff TM is second-countable ) proofend; 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 ) proofend; 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 ) proofend; cluster TopSpace-like second-countable -> Lindelof for TopStruct ; coherence for b1 being TopSpace st b1 is second-countable holds b1 is Lindelof proofend; cluster TopSpace-like regular Lindelof -> normal for TopStruct ; coherence for b1 being TopSpace st b1 is regular & b1 is Lindelof holds b1 is normal proofend; cluster TopSpace-like countable -> Lindelof for TopStruct ; coherence for b1 being TopSpace st b1 is countable holds b1 is Lindelof proofend; end; Lm11: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is second-countable proofend; 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 proofend; end; registration let T be Lindelof TopSpace; let A be closed Subset of T; clusterT | A -> Lindelof ; coherence T | A is Lindelof proofend; end; registration let TM be metrizable Lindelof TopSpace; let A be Subset of TM; clusterTM | A -> Lindelof ; coherence TM | A is Lindelof ; end; definition let T be TopSpace; let A, B, L be Subset of T; predL 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) proofend; 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 ) proofend; :: 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 proofend; :: 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 ) proofend;