:: METRIZTS semantic presentation 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 proof let T1, T2 be empty TopSpace; ::_thesis: T1,T2 are_homeomorphic reconsider E = {} as Function of T1,T2 by FUNCT_2:1, RELAT_1:38; A1: ( [#] T2 = {} iff [#] T1 = {} ) ; for P being Subset of T1 st P is open holds (E ") " P is open ; then A2: E " is continuous by A1, TOPS_2:43; for P being Subset of T2 st P is open holds E " P is open ; then E is continuous by A1, TOPS_2:43; then E is being_homeomorphism by A1, A2, RELAT_1:38, TOPS_2:def_5; hence T1,T2 are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum end; theorem :: METRIZTS:1 for T1, T2 being TopSpace holds ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic ) proof let T1, T2 be TopSpace; ::_thesis: ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic ) A1: ( T1 | ([#] T1) = TopStruct(# the carrier of T1, the topology of T1 #) & T2 | ([#] T2) = TopStruct(# the carrier of T2, the topology of T2 #) ) by TSEP_1:93; percases ( not T2 is empty or T2 is empty ) ; supposeA2: not T2 is empty ; ::_thesis: ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic ) hereby ::_thesis: ( [#] T1, [#] T2 are_homeomorphic implies T1,T2 are_homeomorphic ) assume T1,T2 are_homeomorphic ; ::_thesis: [#] T1, [#] T2 are_homeomorphic then TopStruct(# the carrier of T1, the topology of T1 #), TopStruct(# the carrier of T2, the topology of T2 #) are_homeomorphic by A2, TOPREALA:15; hence [#] T1, [#] T2 are_homeomorphic by A1, Def1; ::_thesis: verum end; assume [#] T1, [#] T2 are_homeomorphic ; ::_thesis: T1,T2 are_homeomorphic then TopStruct(# the carrier of T1, the topology of T1 #), TopStruct(# the carrier of T2, the topology of T2 #) are_homeomorphic by A1, Def1; hence T1,T2 are_homeomorphic by A2, TOPREALA:15; ::_thesis: verum end; supposeA3: T2 is empty ; ::_thesis: ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic ) hereby ::_thesis: ( [#] T1, [#] T2 are_homeomorphic implies T1,T2 are_homeomorphic ) assume T1,T2 are_homeomorphic ; ::_thesis: [#] T1, [#] T2 are_homeomorphic then ( T1 is empty iff T2 is empty ) by YELLOW14:18; then T1 | ([#] T1),T2 | ([#] T2) are_homeomorphic by A3, Lm1; hence [#] T1, [#] T2 are_homeomorphic by Def1; ::_thesis: verum end; assume [#] T1, [#] T2 are_homeomorphic ; ::_thesis: T1,T2 are_homeomorphic then T1 | ([#] T1),T2 | ([#] T2) are_homeomorphic by Def1; then T1 is empty by A3, YELLOW14:18; hence T1,T2 are_homeomorphic by A3, Lm1; ::_thesis: verum end; end; 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 let T1, T2 be TopSpace; ::_thesis: 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 let A1 be Subset of T1; ::_thesis: 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 let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds g is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds g is being_homeomorphism A2: dom f = [#] T1 by A1, TOPS_2:def_5; T1,T2 are_homeomorphic by A1, T_0TOPSP:def_1; then ( T1 is empty iff T2 is empty ) by YELLOW14:18; then A3: ( [#] T1 = {} iff [#] T2 = {} ) ; A4: rng f = [#] T2 by A1, TOPS_2:def_5; set B = f .: A1; let g be Function of (T1 | A1),(T2 | (f .: A1)); ::_thesis: ( g = f | A1 implies g is being_homeomorphism ) assume A5: g = f | A1 ; ::_thesis: g is being_homeomorphism A6: rng g = f .: A1 by A5, RELAT_1:115; A7: f is one-to-one by A1, TOPS_2:def_5; then A8: g is one-to-one by A5, FUNCT_1:52; A9: dom g = (dom f) /\ A1 by A5, RELAT_1:61 .= A1 by A2, XBOOLE_1:28 ; set TA = T1 | A1; set TB = T2 | (f .: A1); A10: [#] (T1 | A1) = A1 by PRE_TOPC:def_5; A11: ( [#] (T1 | A1) = {} iff [#] (T2 | (f .: A1)) = {} ) by A9; A12: [#] (T2 | (f .: A1)) = f .: A1 by PRE_TOPC:def_5; A13: f is continuous by A1, TOPS_2:def_5; for P being Subset of (T2 | (f .: A1)) st P is open holds g " P is open proof let P be Subset of (T2 | (f .: A1)); ::_thesis: ( P is open implies g " P is open ) assume P is open ; ::_thesis: g " P is open then consider P1 being Subset of T2 such that A14: P1 is open and A15: P = P1 /\ (f .: A1) by A12, TSP_1:def_1; reconsider PA = (f " P1) /\ A1 as Subset of (T1 | A1) by A10, XBOOLE_1:17; A1 = f " (f .: A1) by A2, A7, FUNCT_1:94; then ( A1 /\ PA = PA & PA = f " P ) by A15, FUNCT_1:68, XBOOLE_1:17, XBOOLE_1:28; then A16: g " P = PA by A5, FUNCT_1:70; f " P1 is open by A3, A13, A14, TOPS_2:43; hence g " P is open by A10, A16, TSP_1:def_1; ::_thesis: verum end; then A17: g is continuous by A11, TOPS_2:43; A18: f " is continuous by A1, TOPS_2:def_5; for P being Subset of (T1 | A1) st P is open holds (g ") " P is open proof let P be Subset of (T1 | A1); ::_thesis: ( P is open implies (g ") " P is open ) assume P is open ; ::_thesis: (g ") " P is open then consider P1 being Subset of T1 such that A19: P1 is open and A20: P = P1 /\ A1 by A10, TSP_1:def_1; reconsider PB = ((f ") " P1) /\ (f .: A1) as Subset of (T2 | (f .: A1)) by A12, XBOOLE_1:17; A21: (f ") " P1 is open by A3, A18, A19, TOPS_2:43; f .: A1 = (f ") " A1 by A4, A7, TOPS_2:54; then PB = (f ") " (P1 /\ A1) by FUNCT_1:68 .= f .: P by A4, A7, A20, TOPS_2:54 .= g .: P by A5, A10, RELAT_1:129 .= (g ") " P by A6, A8, A12, TOPS_2:54 ; hence (g ") " P is open by A12, A21, TSP_1:def_1; ::_thesis: verum end; then g " is continuous by A11, TOPS_2:43; hence g is being_homeomorphism by A6, A9, A10, A8, A12, A17, TOPS_2:def_5; ::_thesis: verum 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 let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1 for f being Function of T1,T2 st f is being_homeomorphism holds A1,f .: A1 are_homeomorphic let A1 be Subset of T1; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds A1,f .: A1 are_homeomorphic let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies A1,f .: A1 are_homeomorphic ) assume A1: f is being_homeomorphism ; ::_thesis: A1,f .: A1 are_homeomorphic dom f = [#] T1 by A1, TOPS_2:def_5; then A2: dom (f | A1) = ([#] T1) /\ A1 by RELAT_1:61 .= A1 by XBOOLE_1:28 .= [#] (T1 | A1) by PRE_TOPC:def_5 ; rng (f | A1) = f .: A1 by RELAT_1:115 .= [#] (T2 | (f .: A1)) by PRE_TOPC:def_5 ; then reconsider g = f | A1 as Function of (T1 | A1),(T2 | (f .: A1)) by A2, FUNCT_2:1; g is being_homeomorphism by A1, Th2; then T1 | A1,T2 | (f .: A1) are_homeomorphic by T_0TOPSP:def_1; hence A1,f .: A1 are_homeomorphic by Def1; ::_thesis: verum end; Lm2: for T1, T2 being non empty TopSpace st T1,T2 are_homeomorphic holds weight T2 c= weight T1 proof let T1, T2 be non empty TopSpace; ::_thesis: ( T1,T2 are_homeomorphic implies weight T2 c= weight T1 ) defpred S1[ set ] means verum; consider B1 being Basis of T1 such that A1: card B1 = weight T1 by WAYBEL23:74; assume T1,T2 are_homeomorphic ; ::_thesis: weight T2 c= weight T1 then consider f being Function of T1,T2 such that A2: f is being_homeomorphism by T_0TOPSP:def_1; deffunc H1( Subset of T1) -> Element of bool the carrier of T2 = f .: $1; defpred S2[ set ] means ( $1 in B1 & S1[$1] ); A3: card { H1(w) where w is Subset of T1 : S2[w] } c= card B1 from BORSUK_2:sch_1(); consider B2 being Subset-Family of T2 such that A4: B2 = { H1(w) where w is Subset of T1 : S2[w] } from LMOD_7:sch_5(); A5: for A being Subset of T2 st A is open holds for p being Point of T2 st p in A holds ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) proof let A be Subset of T2; ::_thesis: ( A is open implies for p being Point of T2 st p in A holds ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of T2 st p in A holds ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) then A6: f " A is open by A2, TOPGRP_1:26; let p be Point of T2; ::_thesis: ( p in A implies ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) ) assume A7: p in A ; ::_thesis: ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) A8: rng f = [#] T2 by A2, TOPGRP_1:25; then consider x being set such that A9: x in dom f and A10: f . x = p by FUNCT_1:def_3; A11: x in f " A by A7, A9, A10, FUNCT_1:def_7; reconsider x = x as Point of T1 by A9; consider a1 being Subset of T1 such that A12: ( a1 in B1 & x in a1 ) and A13: a1 c= f " A by A6, A11, YELLOW_9:31; take a = H1(a1); ::_thesis: ( a in B2 & p in a & a c= A ) a c= f .: (f " A) by A13, RELAT_1:123; hence ( a in B2 & p in a & a c= A ) by A4, A8, A9, A10, A12, FUNCT_1:77, FUNCT_1:def_6; ::_thesis: verum end; A14: B1 c= the topology of T1 by TOPS_2:64; B2 c= the topology of T2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B2 or x in the topology of T2 ) assume x in B2 ; ::_thesis: x in the topology of T2 then consider w being Subset of T1 such that A15: x = H1(w) and A16: S2[w] by A4; w is open by A14, A16, PRE_TOPC:def_2; then H1(w) is open by A2, TOPGRP_1:25; hence x in the topology of T2 by A15, PRE_TOPC:def_2; ::_thesis: verum end; then reconsider B2 = B2 as Basis of T2 by A5, YELLOW_9:32; weight T2 c= card B2 by WAYBEL23:73; hence weight T2 c= weight T1 by A1, A4, A3, XBOOLE_1:1; ::_thesis: verum end; Lm3: for T being empty TopSpace holds weight T is empty proof let T be empty TopSpace; ::_thesis: weight T is empty reconsider B = {} as empty Subset-Family of T by TOPGEN_4:18; ( B c= the topology of T & ( for A being Subset of T st A is open holds for p being Point of T st p in A holds ex a being Subset of T st ( a in B & p in a & a c= A ) ) ) by XBOOLE_1:2; then reconsider B = B as Basis of T by YELLOW_9:32; weight T c= card B by WAYBEL23:73; hence weight T is empty ; ::_thesis: verum end; theorem Th4: :: METRIZTS:4 for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds weight T1 = weight T2 proof let T1, T2 be TopSpace; ::_thesis: ( T1,T2 are_homeomorphic implies weight T1 = weight T2 ) assume A1: T1,T2 are_homeomorphic ; ::_thesis: weight T1 = weight T2 percases ( [#] T1 = {} or [#] T2 = {} or ( not T1 is empty & not T2 is empty ) ) ; supposeA2: ( [#] T1 = {} or [#] T2 = {} ) ; ::_thesis: weight T1 = weight T2 A3: ( T1 is empty iff T2 is empty ) by A1, YELLOW14:18; then weight T1 = 0 by A2, Lm3; hence weight T1 = weight T2 by A2, A3, Lm3; ::_thesis: verum end; suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: weight T1 = weight T2 then ( weight T2 c= weight T1 & weight T1 c= weight T2 ) by A1, Lm2; hence weight T1 = weight T2 by XBOOLE_0:def_10; ::_thesis: verum end; end; end; registration cluster empty TopSpace-like -> metrizable for TopStruct ; coherence for b1 being TopSpace st b1 is empty holds b1 is metrizable proof let T be TopSpace; ::_thesis: ( T is empty implies T is metrizable ) set cT = the carrier of T; A1: ( dom {} = {} & rng {} c= REAL ) by XBOOLE_1:2; assume A2: T is empty ; ::_thesis: T is metrizable then A3: bool the carrier of T = {{}} by ZFMISC_1:1; the carrier of T = {} by A2; then [: the carrier of T, the carrier of T:] = {} by ZFMISC_1:90; then reconsider E = {} as Function of [: the carrier of T, the carrier of T:],REAL by A1, FUNCT_2:2; set M = SpaceMetr ( the carrier of T,E); take E ; :: according to PCOMPS_1:def_8 ::_thesis: ( E is_metric_of the carrier of T & Family_open_set (SpaceMetr ( the carrier of T,E)) = the topology of T ) for a, b, c being Element of the carrier of T holds ( ( E . (a,b) = 0 implies a = b ) & ( a = b implies E . (a,b) = 0 ) & E . (a,b) = E . (b,a) & E . (a,c) <= (E . (a,b)) + (E . (b,c)) ) proof let a, b, c be Element of the carrier of T; ::_thesis: ( ( E . (a,b) = 0 implies a = b ) & ( a = b implies E . (a,b) = 0 ) & E . (a,b) = E . (b,a) & E . (a,c) <= (E . (a,b)) + (E . (b,c)) ) ( a = {} & b = {} ) by A2, SUBSET_1:def_1; hence ( ( E . (a,b) = 0 implies a = b ) & ( a = b implies E . (a,b) = 0 ) & E . (a,b) = E . (b,a) & E . (a,c) <= (E . (a,b)) + (E . (b,c)) ) ; ::_thesis: verum end; hence E is_metric_of the carrier of T by PCOMPS_1:def_6; ::_thesis: Family_open_set (SpaceMetr ( the carrier of T,E)) = the topology of T then A4: SpaceMetr ( the carrier of T,E) = MetrStruct(# the carrier of T,E #) by PCOMPS_1:def_7; then the carrier of T in Family_open_set (SpaceMetr ( the carrier of T,E)) by PCOMPS_1:30; then Family_open_set (SpaceMetr ( the carrier of T,E)) = {{}} by A3, A4, ZFMISC_1:33; hence Family_open_set (SpaceMetr ( the carrier of T,E)) = the topology of T by A3, ZFMISC_1:33; ::_thesis: verum end; cluster TopSpace-like metrizable -> T_4 for TopStruct ; coherence for b1 being TopSpace st b1 is metrizable holds b1 is T_4 proof let T be TopSpace; ::_thesis: ( T is metrizable implies T is T_4 ) assume A5: T is metrizable ; ::_thesis: T is T_4 percases ( T is empty or not T is empty ) ; supposeA6: T is empty ; ::_thesis: T is T_4 then 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 ) ; then T is normal by PRE_TOPC:def_12; hence T is T_4 by A6; ::_thesis: verum end; suppose not T is empty ; ::_thesis: T is T_4 then reconsider t = T as non empty metrizable TopSpace by A5; ( t is regular & ex Bn being FamilySequence of t st Bn is Basis_sigma_locally_finite ) by NAGATA_2:19; then ( t is T_1 & T is normal ) by NAGATA_1:20, NAGATA_2:19; hence T is T_4 ; ::_thesis: verum end; end; end; let M be MetrSpace; cluster TopSpaceMetr M -> metrizable ; coherence TopSpaceMetr M is metrizable proof percases ( M is empty or not M is empty ) ; suppose M is empty ; ::_thesis: TopSpaceMetr M is metrizable then TopSpaceMetr M is empty ; hence TopSpaceMetr M is metrizable ; ::_thesis: verum end; suppose not M is empty ; ::_thesis: TopSpaceMetr M is metrizable then reconsider m = M as non empty MetrSpace ; set TM = TopSpaceMetr M; reconsider CM = [#] M as non empty Subset of m ; reconsider CTM = [#] (TopSpaceMetr M) as Subset of (TopSpaceMetr M) ; set TMM = TopSpaceMetr (m | CM); A7: [#] (m | CM) = CM by TOPMETR:def_2; then reconsider D = the distance of (m | CM) as Function of [: the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M):],REAL ; take D ; :: according to PCOMPS_1:def_8 ::_thesis: ( D is_metric_of the carrier of (TopSpaceMetr M) & Family_open_set (SpaceMetr ( the carrier of (TopSpaceMetr M),D)) = the topology of (TopSpaceMetr M) ) A8: D is_metric_of the carrier of (TopSpaceMetr M) by A7, PCOMPS_1:35; ( (TopSpaceMetr M) | CTM = TopSpaceMetr (m | CM) & TopSpaceMetr M is SubSpace of TopSpaceMetr M ) by HAUSDORF:16, TSEP_1:2; then the topology of (TopSpaceMetr M) = the topology of (TopSpaceMetr (m | CM)) by A7, TSEP_1:5 .= Family_open_set (SpaceMetr ( the carrier of (TopSpaceMetr M),D)) by A7, A8, PCOMPS_1:def_7 ; hence ( D is_metric_of the carrier of (TopSpaceMetr M) & Family_open_set (SpaceMetr ( the carrier of (TopSpaceMetr M),D)) = the topology of (TopSpaceMetr M) ) by A7, PCOMPS_1:35; ::_thesis: verum end; end; end; end; registration let TM be metrizable TopSpace; let Am be Subset of TM; clusterTM | Am -> metrizable ; coherence TM | Am is metrizable proof percases ( Am is empty or not Am is empty ) ; suppose Am is empty ; ::_thesis: TM | Am is metrizable hence TM | Am is metrizable ; ::_thesis: verum end; supposeA1: not Am is empty ; ::_thesis: TM | Am is metrizable consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that A2: metr is_metric_of the carrier of TM and A3: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def_8; A4: not TM is empty by A1; then reconsider TMM = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A2, PCOMPS_1:36; reconsider Atm = Am as non empty Subset of TMM by A1, A2, A4, PCOMPS_2:4; reconsider ATM = Atm as non empty Subset of (TopSpaceMetr TMM) ; ( TM is SubSpace of TM & the carrier of (TopSpaceMetr TMM) = the carrier of TM ) by A2, A4, PCOMPS_2:4, TSEP_1:2; then TopSpaceMetr TMM is SubSpace of TM by A3, TMAP_1:6; then A5: (TopSpaceMetr TMM) | ATM is SubSpace of TM by TSEP_1:7; ( (TopSpaceMetr TMM) | ATM = TopSpaceMetr (TMM | Atm) & [#] ((TopSpaceMetr TMM) | ATM) = ATM ) by HAUSDORF:16, PRE_TOPC:def_5; hence TM | Am is metrizable by A5, PRE_TOPC:def_5; ::_thesis: verum end; end; end; end; registration let TM1, TM2 be metrizable TopSpace; cluster[:TM1,TM2:] -> metrizable ; coherence [:TM1,TM2:] is metrizable proof percases ( [:TM1,TM2:] is empty or not [:TM1,TM2:] is empty ) ; suppose [:TM1,TM2:] is empty ; ::_thesis: [:TM1,TM2:] is metrizable hence [:TM1,TM2:] is metrizable ; ::_thesis: verum end; supposeA1: not [:TM1,TM2:] is empty ; ::_thesis: [:TM1,TM2:] is metrizable then A2: not TM2 is empty ; consider metr2 being Function of [: the carrier of TM2, the carrier of TM2:],REAL such that A3: metr2 is_metric_of the carrier of TM2 and A4: Family_open_set (SpaceMetr ( the carrier of TM2,metr2)) = the topology of TM2 by PCOMPS_1:def_8; set tm2 = SpaceMetr ( the carrier of TM2,metr2); consider metr1 being Function of [: the carrier of TM1, the carrier of TM1:],REAL such that A5: metr1 is_metric_of the carrier of TM1 and A6: Family_open_set (SpaceMetr ( the carrier of TM1,metr1)) = the topology of TM1 by PCOMPS_1:def_8; set tm1 = SpaceMetr ( the carrier of TM1,metr1); A7: not TM1 is empty by A1; then reconsider tm1 = SpaceMetr ( the carrier of TM1,metr1), tm2 = SpaceMetr ( the carrier of TM2,metr2) as non empty MetrStruct by A5, A3, A2, PCOMPS_1:36; A8: TopStruct(# the carrier of TM2, the topology of TM2 #) = TopStruct(# the carrier of (TopSpaceMetr tm2), the topology of (TopSpaceMetr tm2) #) by A3, A4, A2, PCOMPS_2:4; TopStruct(# the carrier of TM1, the topology of TM1 #) = TopStruct(# the carrier of (TopSpaceMetr tm1), the topology of (TopSpaceMetr tm1) #) by A7, A5, A6, PCOMPS_2:4; then [:TM1,TM2:] = [:(TopSpaceMetr tm1),(TopSpaceMetr tm2):] by A8, WAYBEL29:7 .= TopSpaceMetr (max-Prod2 (tm1,tm2)) by TOPREAL7:23 ; hence [:TM1,TM2:] is metrizable ; ::_thesis: verum end; end; 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 let T1, T2 be TopSpace; ::_thesis: weight [:T1,T2:] c= (weight T1) *` (weight T2) percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ; suppose ( T1 is empty or T2 is empty ) ; ::_thesis: weight [:T1,T2:] c= (weight T1) *` (weight T2) hence weight [:T1,T2:] c= (weight T1) *` (weight T2) ; ::_thesis: verum end; supposeA1: ( not T1 is empty & not T2 is empty ) ; ::_thesis: weight [:T1,T2:] c= (weight T1) *` (weight T2) consider B2 being Basis of T2 such that A2: card B2 = weight T2 by WAYBEL23:74; consider B1 being Basis of T1 such that A3: card B1 = weight T1 by WAYBEL23:74; reconsider B12 = { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } as Basis of [:T1,T2:] by A1, YELLOW_9:40; reconsider B1 = B1, B2 = B2, B12 = B12 as non empty set by A1, YELLOW12:34; deffunc H1( Element of [:B1,B2:]) -> set = [:($1 `1),($1 `2):]; A4: for x being Element of [:B1,B2:] holds H1(x) is Element of B12 proof let x be Element of [:B1,B2:]; ::_thesis: H1(x) is Element of B12 ( x `1 in B1 & x `2 in B2 ) ; then H1(x) in B12 ; hence H1(x) is Element of B12 ; ::_thesis: verum end; consider f being Function of [:B1,B2:],B12 such that A5: for x being Element of [:B1,B2:] holds f . x = H1(x) from FUNCT_2:sch_9(A4); A6: dom f = [:B1,B2:] by FUNCT_2:def_1; B12 c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B12 or x in rng f ) assume x in B12 ; ::_thesis: x in rng f then consider a being Subset of T1, b being Subset of T2 such that A7: x = [:a,b:] and A8: ( a in B1 & b in B2 ) ; reconsider ab = [a,b] as Element of [:B1,B2:] by A8, ZFMISC_1:87; ( [a,b] `1 = a & [a,b] `2 = b ) by MCART_1:7; then x = f . ab by A5, A7; hence x in rng f by A6, FUNCT_1:def_3; ::_thesis: verum end; then A9: ( weight [:T1,T2:] c= card B12 & card B12 c= card [:B1,B2:] ) by A6, CARD_1:12, WAYBEL23:73; card [:B1,B2:] = card [:(card B1),(card B2):] by CARD_2:7 .= (card B1) *` (card B2) by CARD_2:def_2 ; hence weight [:T1,T2:] c= (weight T1) *` (weight T2) by A3, A2, A9, XBOOLE_1:1; ::_thesis: verum end; end; 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 let T1, T2 be TopSpace; ::_thesis: ( not T1 is empty & not T2 is empty implies ( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] ) ) defpred S1[ set ] means verum; set PR2 = pr2 ( the carrier of T1, the carrier of T2); set PR1 = pr1 ( the carrier of T1, the carrier of T2); assume ( not T1 is empty & not T2 is empty ) ; ::_thesis: ( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] ) then reconsider t1 = T1, t2 = T2 as non empty TopSpace ; reconsider T12 = [:t1,t2:] as non empty TopSpace ; consider B12 being Basis of T12 such that A1: card B12 = weight T12 by WAYBEL23:74; deffunc H1( Subset of T12) -> Element of bool the carrier of T1 = (pr1 ( the carrier of T1, the carrier of T2)) .: $1; defpred S2[ set ] means ( $1 in B12 & S1[$1] ); consider B1 being Subset-Family of T1 such that A2: B1 = { H1(w) where w is Subset of T12 : S2[w] } from LMOD_7:sch_5(); A3: B12 c= the topology of T12 by TOPS_2:64; A4: B1 c= the topology of T1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B1 or x in the topology of T1 ) assume x in B1 ; ::_thesis: x in the topology of T1 then consider w being Subset of T12 such that A5: x = H1(w) and A6: S2[w] by A2; w is open by A3, A6, PRE_TOPC:def_2; then H1(w) is open by BORSUK_1:18; hence x in the topology of T1 by A5, PRE_TOPC:def_2; ::_thesis: verum end; for A being Subset of T1 st A is open holds for p being Point of T1 st p in A holds ex a being Subset of T1 st ( a in B1 & p in a & a c= A ) proof let A be Subset of T1; ::_thesis: ( A is open implies for p being Point of T1 st p in A holds ex a being Subset of T1 st ( a in B1 & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of T1 st p in A holds ex a being Subset of T1 st ( a in B1 & p in a & a c= A ) then A7: [:A,([#] T2):] is open by BORSUK_1:6; set p2 = the Point of T2; A8: the Point of T2 in [#] t2 ; let p1 be Point of T1; ::_thesis: ( p1 in A implies ex a being Subset of T1 st ( a in B1 & p1 in a & a c= A ) ) assume p1 in A ; ::_thesis: ex a being Subset of T1 st ( a in B1 & p1 in a & a c= A ) then A9: [p1, the Point of T2] in [:A,([#] T2):] by A8, ZFMISC_1:87; then reconsider p = [p1, the Point of T2] as Point of T12 ; consider a12 being Subset of T12 such that A10: a12 in B12 and A11: p in a12 and A12: a12 c= [:A,([#] T2):] by A7, A9, YELLOW_9:31; ( p1 in [#] t1 & the Point of T2 in [#] t2 ) ; then A13: (pr1 ( the carrier of T1, the carrier of T2)) . (p1, the Point of T2) = p1 by FUNCT_3:def_4; a12 is open by A3, A10, PRE_TOPC:def_2; then reconsider a = H1(a12) as open Subset of T1 by BORSUK_1:18; take a ; ::_thesis: ( a in B1 & p1 in a & a c= A ) dom (pr1 ( the carrier of T1, the carrier of T2)) = [:([#] T1),([#] T2):] by FUNCT_3:def_4 .= [#] T12 by BORSUK_1:def_2 ; hence ( a in B1 & p1 in a ) by A2, A10, A11, A13, FUNCT_1:def_6; ::_thesis: a c= A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in A ) assume y in a ; ::_thesis: y in A then consider x being set such that A14: x in dom (pr1 ( the carrier of T1, the carrier of T2)) and A15: ( x in a12 & y = (pr1 ( the carrier of T1, the carrier of T2)) . x ) by FUNCT_1:def_6; consider x1, x2 being set such that A16: ( x1 in [#] T1 & x2 in [#] T2 ) and A17: x = [x1,x2] by A14, ZFMISC_1:def_2; (pr1 ( the carrier of T1, the carrier of T2)) . (x1,x2) = x1 by A16, FUNCT_3:def_4; hence y in A by A12, A15, A17, ZFMISC_1:87; ::_thesis: verum end; then reconsider B1 = B1 as Basis of T1 by A4, YELLOW_9:32; A18: card { H1(w) where w is Subset of T12 : S2[w] } c= card B12 from BORSUK_2:sch_1(); weight t1 c= card B1 by WAYBEL23:73; hence weight T1 c= weight [:T1,T2:] by A1, A2, A18, XBOOLE_1:1; ::_thesis: weight T2 c= weight [:T1,T2:] deffunc H2( Subset of T12) -> Element of bool the carrier of T2 = (pr2 ( the carrier of T1, the carrier of T2)) .: $1; consider B2 being Subset-Family of T2 such that A19: B2 = { H2(w) where w is Subset of T12 : S2[w] } from LMOD_7:sch_5(); A20: for A being Subset of T2 st A is open holds for p being Point of T2 st p in A holds ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) proof let A be Subset of T2; ::_thesis: ( A is open implies for p being Point of T2 st p in A holds ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of T2 st p in A holds ex a being Subset of T2 st ( a in B2 & p in a & a c= A ) then A21: [:([#] T1),A:] is open by BORSUK_1:6; set p1 = the Point of T1; A22: the Point of T1 in [#] t1 ; let p2 be Point of T2; ::_thesis: ( p2 in A implies ex a being Subset of T2 st ( a in B2 & p2 in a & a c= A ) ) assume p2 in A ; ::_thesis: ex a being Subset of T2 st ( a in B2 & p2 in a & a c= A ) then A23: [ the Point of T1,p2] in [:([#] T1),A:] by A22, ZFMISC_1:87; then reconsider p = [ the Point of T1,p2] as Point of T12 ; consider a12 being Subset of T12 such that A24: a12 in B12 and A25: p in a12 and A26: a12 c= [:([#] T1),A:] by A21, A23, YELLOW_9:31; ( the Point of T1 in [#] t1 & p2 in [#] t2 ) ; then A27: (pr2 ( the carrier of T1, the carrier of T2)) . ( the Point of T1,p2) = p2 by FUNCT_3:def_5; a12 is open by A3, A24, PRE_TOPC:def_2; then reconsider a = H2(a12) as open Subset of T2 by BORSUK_1:18; take a ; ::_thesis: ( a in B2 & p2 in a & a c= A ) dom (pr2 ( the carrier of T1, the carrier of T2)) = [:([#] T1),([#] T2):] by FUNCT_3:def_5 .= [#] T12 by BORSUK_1:def_2 ; hence ( a in B2 & p2 in a ) by A19, A24, A25, A27, FUNCT_1:def_6; ::_thesis: a c= A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in A ) assume y in a ; ::_thesis: y in A then consider x being set such that A28: x in dom (pr2 ( the carrier of T1, the carrier of T2)) and A29: ( x in a12 & y = (pr2 ( the carrier of T1, the carrier of T2)) . x ) by FUNCT_1:def_6; consider x1, x2 being set such that A30: ( x1 in [#] T1 & x2 in [#] T2 ) and A31: x = [x1,x2] by A28, ZFMISC_1:def_2; (pr2 ( the carrier of T1, the carrier of T2)) . (x1,x2) = x2 by A30, FUNCT_3:def_5; hence y in A by A26, A29, A31, ZFMISC_1:87; ::_thesis: verum end; B2 c= the topology of T2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B2 or x in the topology of T2 ) assume x in B2 ; ::_thesis: x in the topology of T2 then consider w being Subset of T12 such that A32: x = H2(w) and A33: S2[w] by A19; w is open by A3, A33, PRE_TOPC:def_2; then H2(w) is open by BORSUK_1:18; hence x in the topology of T2 by A32, PRE_TOPC:def_2; ::_thesis: verum end; then reconsider B2 = B2 as Basis of T2 by A20, YELLOW_9:32; A34: card { H2(w) where w is Subset of T12 : S2[w] } c= card B12 from BORSUK_2:sch_1(); weight T2 c= card B2 by WAYBEL23:73; hence weight T2 c= weight [:T1,T2:] by A1, A19, A34, XBOOLE_1:1; ::_thesis: verum end; registration let T1, T2 be second-countable TopSpace; cluster[:T1,T2:] -> second-countable ; coherence [:T1,T2:] is second-countable proof ( weight T1 c= omega & weight T2 c= omega ) by WAYBEL23:def_6; then A1: (weight T1) *` (weight T2) c= omega by CARD_2:90, CARD_4:6; weight [:T1,T2:] c= (weight T1) *` (weight T2) by Th5; then weight [:T1,T2:] c= omega by A1, XBOOLE_1:1; hence [:T1,T2:] is second-countable by WAYBEL23:def_6; ::_thesis: verum 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 let T be TopSpace; ::_thesis: for A being Subset of T for F being Subset-Family of T holds card (F | A) c= card F let A be Subset of T; ::_thesis: for F being Subset-Family of T holds card (F | A) c= card F let F be Subset-Family of T; ::_thesis: card (F | A) c= card F set FA = F | A; percases ( F | A is empty or not F | A is empty ) ; suppose F | A is empty ; ::_thesis: card (F | A) c= card F hence card (F | A) c= card F ; ::_thesis: verum end; supposeA1: not F | A is empty ; ::_thesis: card (F | A) c= card F deffunc H1( set ) -> Element of bool the carrier of T = $1 /\ A; A2: A = [#] (T | A) by PRE_TOPC:def_5; A3: for x being set st x in F holds H1(x) in F | A proof let x be set ; ::_thesis: ( x in F implies H1(x) in F | A ) A4: H1(x) c= A by XBOOLE_1:17; assume x in F ; ::_thesis: H1(x) in F | A hence H1(x) in F | A by A2, A4, TOPS_2:def_3; ::_thesis: verum end; consider g being Function of F,(F | A) such that A5: for x being set st x in F holds g . x = H1(x) from FUNCT_2:sch_2(A3); A6: dom g = F by A1, FUNCT_2:def_1; F | A c= rng g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F | A or x in rng g ) assume x in F | A ; ::_thesis: x in rng g then consider B being Subset of T such that A7: B in F and A8: H1(B) = x by TOPS_2:def_3; x = g . B by A5, A7, A8; hence x in rng g by A6, A7, FUNCT_1:def_3; ::_thesis: verum end; hence card (F | A) c= card F by A6, CARD_1:12; ::_thesis: verum end; end; 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 let T be TopSpace; ::_thesis: for A being Subset of T for Bas being Basis of T holds Bas | A is Basis of (T | A) let A be Subset of T; ::_thesis: for Bas being Basis of T holds Bas | A is Basis of (T | A) let Bas be Basis of T; ::_thesis: Bas | A is Basis of (T | A) set BasA = Bas | A; set TA = T | A; A1: for U being Subset of (T | A) st U is open holds for p being Point of (T | A) st p in U holds ex a being Subset of (T | A) st ( a in Bas | A & p in a & a c= U ) proof let U be Subset of (T | A); ::_thesis: ( U is open implies for p being Point of (T | A) st p in U holds ex a being Subset of (T | A) st ( a in Bas | A & p in a & a c= U ) ) assume U is open ; ::_thesis: for p being Point of (T | A) st p in U holds ex a being Subset of (T | A) st ( a in Bas | A & p in a & a c= U ) then consider W being Subset of T such that A2: W is open and A3: U = W /\ the carrier of (T | A) by TSP_1:def_1; let p be Point of (T | A); ::_thesis: ( p in U implies ex a being Subset of (T | A) st ( a in Bas | A & p in a & a c= U ) ) assume A4: p in U ; ::_thesis: ex a being Subset of (T | A) st ( a in Bas | A & p in a & a c= U ) p in W by A3, A4, XBOOLE_0:def_4; then consider Wb being Subset of T such that A5: Wb in Bas and A6: p in Wb and A7: Wb c= W by A2, YELLOW_9:31; A8: Wb /\ A in Bas | A by A5, TOPS_2:31; then reconsider WbA = Wb /\ A as Subset of (T | A) ; A9: [#] (T | A) = A by PRE_TOPC:def_5; then p in WbA by A4, A6, XBOOLE_0:def_4; hence ex a being Subset of (T | A) st ( a in Bas | A & p in a & a c= U ) by A3, A7, A8, A9, XBOOLE_1:26; ::_thesis: verum end; Bas | A c= the topology of (T | A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Bas | A or x in the topology of (T | A) ) assume A10: x in Bas | A ; ::_thesis: x in the topology of (T | A) reconsider U = x as Subset of (T | A) by A10; Bas | A is open by TOPS_2:37; then U is open by A10, TOPS_2:def_1; hence x in the topology of (T | A) by PRE_TOPC:def_2; ::_thesis: verum end; hence Bas | A is Basis of (T | A) by A1, YELLOW_9:32; ::_thesis: verum end; registration let T be second-countable TopSpace; let A be Subset of T; clusterT | A -> second-countable ; coherence T | A is second-countable proof consider B being Basis of T such that A1: card B = weight T by WAYBEL23:74; B | A is Basis of (T | A) by Th8; then A2: weight (T | A) c= card (B | A) by WAYBEL23:73; card (B | A) c= card B by Th7; then ( weight T c= omega & weight (T | A) c= weight T ) by A1, A2, WAYBEL23:def_6, XBOOLE_1:1; then weight (T | A) c= omega by XBOOLE_1:1; hence T | A is second-countable by WAYBEL23:def_6; ::_thesis: verum 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 set d = dist_min A; set TM = TopSpaceMetr M; A1: for P being Subset of R^1 st P is open holds (dist_min A) " P is open proof let P be Subset of R^1; ::_thesis: ( P is open implies (dist_min A) " P is open ) assume A2: P is open ; ::_thesis: (dist_min A) " P is open for p being Point of M st p in (dist_min A) " P holds ex r being real number st ( r > 0 & Ball (p,r) c= (dist_min A) " P ) proof reconsider P9 = P as open Subset of (TopSpaceMetr RealSpace) by A2, TOPMETR:def_6; let p be Point of M; ::_thesis: ( p in (dist_min A) " P implies ex r being real number st ( r > 0 & Ball (p,r) c= (dist_min A) " P ) ) assume p in (dist_min A) " P ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (dist_min A) " P ) then A3: (dist_min A) . p in P by FUNCT_1:def_7; then reconsider dp = (dist_min A) . p as Point of RealSpace by TOPMETR:def_6; consider r being real number such that A4: r > 0 and A5: Ball (dp,r) c= P9 by A3, TOPMETR:15; take r ; ::_thesis: ( r > 0 & Ball (p,r) c= (dist_min A) " P ) thus r > 0 by A4; ::_thesis: Ball (p,r) c= (dist_min A) " P thus Ball (p,r) c= (dist_min A) " P ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (p,r) or x in (dist_min A) " P ) assume A6: x in Ball (p,r) ; ::_thesis: x in (dist_min A) " P then reconsider q = x as Point of M ; A7: dist (p,q) < r by A6, METRIC_1:11; A8: dom (dist_min A) = [#] M by FUNCT_2:def_1; then (dist_min A) . q in rng (dist_min A) by FUNCT_1:def_3; then reconsider dq = (dist_min A) . q as Point of RealSpace by TOPMETR:def_6; (dist_min A) . q <= (dist (q,p)) + ((dist_min A) . p) by HAUSDORF:15; then ((dist_min A) . q) - ((dist_min A) . p) <= dist (p,q) by XREAL_1:20; then A9: - (dist (p,q)) <= - (((dist_min A) . q) - ((dist_min A) . p)) by XREAL_1:24; (dist_min A) . p <= (dist (p,q)) + ((dist_min A) . q) by HAUSDORF:15; then ((dist_min A) . p) - ((dist_min A) . q) <= dist (p,q) by XREAL_1:20; then abs (((dist_min A) . p) - ((dist_min A) . q)) <= dist (p,q) by A9, ABSVALUE:5; then abs (((dist_min A) . p) - ((dist_min A) . q)) < r by A7, XXREAL_0:2; then dist (dp,dq) < r by METRIC_1:def_12; then dq in Ball (dp,r) by METRIC_1:11; hence x in (dist_min A) " P by A5, A8, FUNCT_1:def_7; ::_thesis: verum end; end; hence (dist_min A) " P is open by TOPMETR:15; ::_thesis: verum end; ( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} ) ; hence dist_min A is continuous by A1, TOPS_2:43; ::_thesis: verum 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 let T be TopSpace; ::_thesis: for A, B being Subset of T for F being Subset of (T | A) st F = B holds (T | A) | F = T | B let A, B be Subset of T; ::_thesis: for F being Subset of (T | A) st F = B holds (T | A) | F = T | B let F be Subset of (T | A); ::_thesis: ( F = B implies (T | A) | F = T | B ) assume A1: F = B ; ::_thesis: (T | A) | F = T | B ( (T | A) | F is SubSpace of T & [#] ((T | A) | F) = F ) by PRE_TOPC:def_5, TSEP_1:7; hence (T | A) | F = T | B by A1, PRE_TOPC:def_5; ::_thesis: verum 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 let M be non empty MetrSpace; ::_thesis: 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) set TM = TopSpaceMetr M; let A be non empty Subset of (TopSpaceMetr M); ::_thesis: 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) let r be real number ; ::_thesis: { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M) set d = dist_min A; reconsider A = ].-infty,r.[ as Subset of R^1 by TOPMETR:17; set dA = { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } ; A1: { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } c= (dist_min A) " A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } or x in (dist_min A) " A ) assume x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } ; ::_thesis: x in (dist_min A) " A then consider p being Point of (TopSpaceMetr M) such that A2: p = x and A3: (dist_min A) . p < r ; ( dom (dist_min A) = [#] (TopSpaceMetr M) & (dist_min A) . p in A ) by A3, FUNCT_2:def_1, XXREAL_1:233; hence x in (dist_min A) " A by A2, FUNCT_1:def_7; ::_thesis: verum end; A4: (dist_min A) " A c= { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dist_min A) " A or x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } ) assume A5: x in (dist_min A) " A ; ::_thesis: x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } then reconsider p = x as Point of (TopSpaceMetr M) ; (dist_min A) . p in A by A5, FUNCT_1:def_7; then (dist_min A) . p < r by XXREAL_1:233; hence x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } ; ::_thesis: verum end; A6: A is open by BORSUK_5:40; ( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} ) ; then (dist_min A) " A is open by A6, TOPS_2:43; hence { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M) by A1, A4, XBOOLE_0:def_10; ::_thesis: verum end; 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 set TOP = the topology of TM; set cTM = the carrier of TM; let Am be Subset of TM; ::_thesis: ( Am is open implies Am is F_sigma ) assume A1: Am is open ; ::_thesis: Am is F_sigma percases ( TM is empty or not TM is empty ) ; supposeA2: TM is empty ; ::_thesis: Am is F_sigma reconsider E = {} as empty Subset-Family of TM by TOPGEN_4:18; Am = union E by A2, ZFMISC_1:2; hence Am is F_sigma by TOPGEN_4:def_6; ::_thesis: verum end; supposeA3: not TM is empty ; ::_thesis: Am is F_sigma percases ( Am = [#] TM or Am <> [#] TM ) ; suppose Am = [#] TM ; ::_thesis: Am is F_sigma hence Am is F_sigma by A3; ::_thesis: verum end; supposeA4: Am <> [#] TM ; ::_thesis: Am is F_sigma consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that A5: metr is_metric_of the carrier of TM and A6: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def_8; reconsider Tm = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A3, A5, PCOMPS_1:36; set TTm = TopSpaceMetr Tm; Am in the topology of (TopSpaceMetr Tm) by A1, A6, PRE_TOPC:def_2; then reconsider a = Am as open Subset of (TopSpaceMetr Tm) by PRE_TOPC:def_2; ({} (TopSpaceMetr Tm)) ` = [#] (TopSpaceMetr Tm) ; then reconsider A9 = a ` as non empty closed Subset of (TopSpaceMetr Tm) by A3, A4, A5, PCOMPS_2:4; defpred S1[ set , set ] means for n being Nat st n = TM holds c2 = { p where p is Point of (TopSpaceMetr Tm) : (dist_min A9) . p < 1 / (2 |^ n) } ; A7: for x being set st x in NAT holds ex y being set st ( y in the topology of TM & S1[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in the topology of TM & S1[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in the topology of TM & S1[x,y] ) then reconsider n = x as Element of NAT ; reconsider BallA = { p where p is Point of (TopSpaceMetr Tm) : (dist_min A9) . p < 1 / (2 |^ n) } as open Subset of (TopSpaceMetr Tm) by Lm4; take BallA ; ::_thesis: ( BallA in the topology of TM & S1[x,BallA] ) thus ( BallA in the topology of TM & S1[x,BallA] ) by A6, PRE_TOPC:def_2; ::_thesis: verum end; consider p being Function of NAT, the topology of TM such that A8: for x being set st x in NAT holds S1[x,p . x] from FUNCT_2:sch_1(A7); reconsider RNG = rng p as open Subset-Family of TM by TOPS_2:11, XBOOLE_1:1; set Crng = COMPLEMENT RNG; A9: dom p = NAT by FUNCT_2:def_1; A10: [#] TM = [#] (TopSpaceMetr Tm) by A3, A5, PCOMPS_2:4; A11: union (COMPLEMENT RNG) = Am proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Am c= union (COMPLEMENT RNG) let x be set ; ::_thesis: ( x in union (COMPLEMENT RNG) implies x in Am ) assume A12: x in union (COMPLEMENT RNG) ; ::_thesis: x in Am then consider y being set such that A13: x in y and A14: y in COMPLEMENT RNG by TARSKI:def_4; reconsider Y = y as Subset of TM by A14; Y ` in RNG by A14, SETFAM_1:def_7; then consider n being set such that A15: n in dom p and A16: p . n = Y ` by FUNCT_1:def_3; reconsider n = n as Element of NAT by A15; assume not x in Am ; ::_thesis: contradiction then x in A9 by A10, A12, XBOOLE_0:def_5; then A17: ( 2 |^ n > 0 & (dist_min A9) . x = 0 ) by HAUSDORF:5, PREPOWER:6; Y ` = { q where q is Point of (TopSpaceMetr Tm) : (dist_min A9) . q < 1 / (2 |^ n) } by A8, A16; then x in Y ` by A10, A12, A17; hence contradiction by A13, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Am or x in union (COMPLEMENT RNG) ) assume A18: x in Am ; ::_thesis: x in union (COMPLEMENT RNG) then reconsider q = x as Point of (TopSpaceMetr Tm) by A3, A5, PCOMPS_2:4; ( Cl A9 = A9 & not q in A9 ) by A18, PRE_TOPC:22, XBOOLE_0:def_5; then A19: (dist_min A9) . q <> 0 by HAUSDORF:8; (dist_min A9) . q >= 0 by JORDAN1K:9; then consider n being Element of NAT such that A20: 1 / (2 |^ n) <= (dist_min A9) . q by A19, PREPOWER:92; p . n in RNG by A9, FUNCT_1:def_3; then reconsider pn = p . n as Subset of TM ; A21: pn = { s where s is Point of (TopSpaceMetr Tm) : (dist_min A9) . s < 1 / (2 |^ n) } by A8; for s being Point of (TopSpaceMetr Tm) st s = q holds not 1 / (2 |^ n) > (dist_min A9) . s by A20; then not q in pn by A21; then A22: q in pn ` by A18, XBOOLE_0:def_5; (pn `) ` in RNG by A9, FUNCT_1:def_3; then pn ` in COMPLEMENT RNG by SETFAM_1:def_7; hence x in union (COMPLEMENT RNG) by A22, TARSKI:def_4; ::_thesis: verum end; ( COMPLEMENT RNG is closed & RNG is countable ) by A9, CARD_3:93, TOPS_2:10; hence Am is F_sigma by A11, TOPGEN_4:def_6; ::_thesis: verum end; end; end; end; 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 let Am be Subset of TM; ::_thesis: ( Am is closed implies Am is G_delta ) assume A23: Am is closed ; ::_thesis: Am is G_delta percases ( TM is empty or not TM is empty ) ; supposeA24: TM is empty ; ::_thesis: Am is G_delta reconsider E = {} as empty Subset-Family of TM by TOPGEN_4:18; Am = meet E by A24, SETFAM_1:1; hence Am is G_delta by TOPGEN_4:def_7; ::_thesis: verum end; suppose not TM is empty ; ::_thesis: Am is G_delta then (Am `) ` is G_delta by A23, TOPGEN_4:37; hence Am is G_delta ; ::_thesis: verum end; end; 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 let T be TopSpace; ::_thesis: 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 let B, A be Subset of T; ::_thesis: for F being Subset of (T | B) st A is F_sigma & F = A /\ B holds F is F_sigma let F be Subset of (T | B); ::_thesis: ( A is F_sigma & F = A /\ B implies F is F_sigma ) assume that A1: A is F_sigma and A2: F = A /\ B ; ::_thesis: F is F_sigma consider G being countable closed Subset-Family of T such that A3: A = union G by A1, TOPGEN_4:def_6; A4: union (G | B) c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (G | B) or x in F ) assume x in union (G | B) ; ::_thesis: x in F then consider g being set such that A5: x in g and A6: g in G | B by TARSKI:def_4; consider h being Subset of T such that A7: h in G and A8: h /\ B = g by A6, TOPS_2:def_3; x in h by A5, A8, XBOOLE_0:def_4; then A9: x in A by A3, A7, TARSKI:def_4; x in B by A5, A8, XBOOLE_0:def_4; hence x in F by A2, A9, XBOOLE_0:def_4; ::_thesis: verum end; ( card (G | B) c= card G & card G c= omega ) by Th7, CARD_3:def_14; then card (G | B) c= omega by XBOOLE_1:1; then A10: ( G | B is closed & G | B is countable ) by CARD_3:def_14, TOPS_2:38; (A /\ B) /\ B = A /\ (B /\ B) by XBOOLE_1:16 .= F by A2 ; then F c= union (G | B) by A3, TOPS_2:32, XBOOLE_1:17; then F = union (G | B) by A4, XBOOLE_0:def_10; hence F is F_sigma by A10, TOPGEN_4:def_6; ::_thesis: verum 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 let T be TopSpace; ::_thesis: 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 let B, A be Subset of T; ::_thesis: for F being Subset of (T | B) st A is G_delta & F = A /\ B holds F is G_delta let F be Subset of (T | B); ::_thesis: ( A is G_delta & F = A /\ B implies F is G_delta ) assume that A1: A is G_delta and A2: F = A /\ B ; ::_thesis: F is G_delta consider G being countable open Subset-Family of T such that A3: A = meet G by A1, TOPGEN_4:def_7; A4: meet (G | B) c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (G | B) or x in F ) assume A5: x in meet (G | B) ; ::_thesis: x in F then consider g being set such that A6: g in G | B by SETFAM_1:1, XBOOLE_0:def_1; reconsider g = g as Subset of (T | B) by A6; A7: ex h being Subset of T st ( h in G & h /\ B = g ) by A6, TOPS_2:def_3; x in g by A5, A6, SETFAM_1:def_1; then A8: x in B by A7, XBOOLE_0:def_4; now__::_thesis:_for_Y_being_set_st_Y_in_G_holds_ x_in_Y let Y be set ; ::_thesis: ( Y in G implies x in Y ) assume Y in G ; ::_thesis: x in Y then Y /\ B in G | B by TOPS_2:31; then x in Y /\ B by A5, SETFAM_1:def_1; hence x in Y by XBOOLE_0:def_4; ::_thesis: verum end; then x in A by A3, A7, SETFAM_1:def_1; hence x in F by A2, A8, XBOOLE_0:def_4; ::_thesis: verum end; ( card (G | B) c= card G & card G c= omega ) by Th7, CARD_3:def_14; then card (G | B) c= omega by XBOOLE_1:1; then A9: ( G | B is open & G | B is countable ) by CARD_3:def_14, TOPS_2:37; F c= meet (G | B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in meet (G | B) ) assume A10: x in F ; ::_thesis: x in meet (G | B) then A11: x in A by A2, XBOOLE_0:def_4; A12: x in B by A2, A10, XBOOLE_0:def_4; A13: now__::_thesis:_for_f_being_set_st_f_in_G_|_B_holds_ x_in_f let f be set ; ::_thesis: ( f in G | B implies x in f ) assume f in G | B ; ::_thesis: x in f then consider h being Subset of T such that A14: h in G and A15: h /\ B = f by TOPS_2:def_3; x in h by A3, A11, A14, SETFAM_1:def_1; hence x in f by A12, A15, XBOOLE_0:def_4; ::_thesis: verum end; ex y being set st y in G by A3, A11, SETFAM_1:1, XBOOLE_0:def_1; then not G | B is empty by TOPS_2:31; hence x in meet (G | B) by A13, SETFAM_1:def_1; ::_thesis: verum end; then F = meet (G | B) by A4, XBOOLE_0:def_10; hence F is G_delta by A9, TOPGEN_4:def_7; ::_thesis: verum 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 let T be TopSpace; ::_thesis: for A being Subset of T st T is T_1 & A is discrete holds A is open Subset of (T | (Cl A)) let A be Subset of T; ::_thesis: ( T is T_1 & A is discrete implies A is open Subset of (T | (Cl A)) ) assume that A1: T is T_1 and A2: A is discrete ; ::_thesis: A is open Subset of (T | (Cl A)) set TA = T | (Cl A); A3: [#] (T | (Cl A)) = Cl A by PRE_TOPC:def_5; A4: A c= Cl A by PRE_TOPC:18; percases ( T | (Cl A) is empty or not T | (Cl A) is empty ) ; suppose T | (Cl A) is empty ; ::_thesis: A is open Subset of (T | (Cl A)) hence A is open Subset of (T | (Cl A)) by A3, PRE_TOPC:18; ::_thesis: verum end; suppose not T | (Cl A) is empty ; ::_thesis: A is open Subset of (T | (Cl A)) then reconsider TA = T | (Cl A) as non empty TopSpace ; deffunc H1( Element of TA) -> Element of bool the carrier of TA = {$1}; defpred S1[ set ] means $1 in A; consider S being Subset-Family of TA such that A5: S = { H1(x) where x is Element of TA : S1[x] } from LMOD_7:sch_5(); A6: S is open proof let B be Subset of TA; :: according to TOPS_2:def_1 ::_thesis: ( not B in S or B is open ) assume B in S ; ::_thesis: B is open then consider y being Element of TA such that A7: B = H1(y) and A8: S1[y] by A5; reconsider x = y as Point of T by A8; consider G being Subset of T such that A9: G is open and A10: A /\ G = {x} by A2, A8, TEX_2:26; reconsider X = {x} as Subset of T by A10; not T is empty by A7; then A11: Cl X = X by A1, PRE_TOPC:22; x in {x} by TARSKI:def_1; then ( x in A & x in G ) by A10, XBOOLE_0:def_4; then A12: G /\ (Cl A) <> {} by A4, XBOOLE_0:def_4; G /\ (Cl A) c= Cl X by A9, A10, TOPS_1:13; then G /\ (Cl A) = X by A11, A12, ZFMISC_1:33; hence B is open by A3, A7, A9, TSP_1:def_1; ::_thesis: verum end; union S = A proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= union S let x be set ; ::_thesis: ( x in union S implies x in A ) assume x in union S ; ::_thesis: x in A then consider y being set such that A13: x in y and A14: y in S by TARSKI:def_4; ex z being Element of TA st ( H1(z) = y & S1[z] ) by A5, A14; hence x in A by A13, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union S ) assume x in A ; ::_thesis: x in union S then A15: {x} in S by A3, A4, A5; x in {x} by TARSKI:def_1; hence x in union S by A15, TARSKI:def_4; ::_thesis: verum end; hence A is open Subset of (T | (Cl A)) by A6, TOPS_2:19; ::_thesis: verum end; end; end; Lm5: for iC being infinite Cardinal holds omega *` iC = iC proof let iC be infinite Cardinal; ::_thesis: omega *` iC = iC omega c= iC by CARD_3:85; then A1: omega *` iC c= iC *` iC by CARD_2:90; ( iC *` iC = iC & iC c= omega *` iC ) by CARD_2:95, CARD_4:15; hence omega *` iC = iC by A1, XBOOLE_0:def_10; ::_thesis: verum 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 let C be Cardinal; ::_thesis: 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 let T be TopSpace; ::_thesis: ( ( 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 ) ) implies for A being Subset of T st A is closed & A is discrete holds card A c= C ) assume A1: 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 ) ; ::_thesis: for A being Subset of T st A is closed & A is discrete holds card A c= C set TOP = the topology of T; let A be Subset of T; ::_thesis: ( A is closed & A is discrete implies card A c= C ) assume that A2: A is closed and A3: A is discrete ; ::_thesis: card A c= C A ` in the topology of T by A2, PRE_TOPC:def_2; then A4: {(A `)} c= the topology of T by ZFMISC_1:31; defpred S1[ set , set ] means {$2} = $1 /\ A; defpred S2[ set , set ] means A /\ $2 = {$1}; A5: for x being set st x in A holds ex y being set st ( y in the topology of T & S2[x,y] ) proof let x be set ; ::_thesis: ( x in A implies ex y being set st ( y in the topology of T & S2[x,y] ) ) assume x in A ; ::_thesis: ex y being set st ( y in the topology of T & S2[x,y] ) then consider G being Subset of T such that A6: ( G is open & A /\ G = {x} ) by A3, TEX_2:26; take G ; ::_thesis: ( G in the topology of T & S2[x,G] ) thus ( G in the topology of T & S2[x,G] ) by A6, PRE_TOPC:def_2; ::_thesis: verum end; consider p being Function of A, the topology of T such that A7: for x being set st x in A holds S2[x,p . x] from FUNCT_2:sch_1(A5); reconsider RNG = rng p, AA = {(A `)} as open Subset-Family of T by A4, TOPS_2:11, XBOOLE_1:1; reconsider RngA = RNG \/ AA as open Subset-Family of T by TOPS_2:13; [#] T c= union RngA proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in union RngA ) assume A8: x in [#] T ; ::_thesis: x in union RngA percases ( x in A or not x in A ) ; supposeA9: x in A ; ::_thesis: x in union RngA dom p = A by FUNCT_2:def_1; then p . x in rng p by A9, FUNCT_1:def_3; then A10: p . x in RngA by XBOOLE_0:def_3; ( x in {x} & A /\ (p . x) = {x} ) by A7, A9, TARSKI:def_1; then x in p . x by XBOOLE_0:def_4; hence x in union RngA by A10, TARSKI:def_4; ::_thesis: verum end; supposeA11: not x in A ; ::_thesis: x in union RngA A ` in AA by TARSKI:def_1; then A12: A ` in RngA by XBOOLE_0:def_3; x in A ` by A8, A11, XBOOLE_0:def_5; hence x in union RngA by A12, TARSKI:def_4; ::_thesis: verum end; end; end; then RngA is Cover of T by SETFAM_1:def_11; then consider G being Subset-Family of T such that A13: G c= RngA and A14: G is Cover of T and A15: card G c= C by A1; A16: for x being set st x in G \ AA holds ex y being set st ( y in A & S1[x,y] ) proof let x be set ; ::_thesis: ( x in G \ AA implies ex y being set st ( y in A & S1[x,y] ) ) assume x in G \ AA ; ::_thesis: ex y being set st ( y in A & S1[x,y] ) then ( x in G & not x in AA ) by XBOOLE_0:def_5; then x in RNG by A13, XBOOLE_0:def_3; then consider y being set such that A17: ( y in dom p & p . y = x ) by FUNCT_1:def_3; take y ; ::_thesis: ( y in A & S1[x,y] ) thus ( y in A & S1[x,y] ) by A7, A17; ::_thesis: verum end; consider q being Function of (G \ AA),A such that A18: for x being set st x in G \ AA holds S1[x,q . x] from FUNCT_2:sch_1(A16); percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: card A c= C hence card A c= C ; ::_thesis: verum end; suppose not A is empty ; ::_thesis: card A c= C then A19: dom q = G \ AA by FUNCT_2:def_1; A c= rng q proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng q ) assume A20: x in A ; ::_thesis: x in rng q not T is empty by A20; then consider U being Subset of T such that A21: x in U and A22: U in G by A14, A20, PCOMPS_1:3; not x in A ` by A20, XBOOLE_0:def_5; then not U in AA by A21, TARSKI:def_1; then U in G \ AA by A22, XBOOLE_0:def_5; then A23: ( q . U in rng q & {(q . U)} = U /\ A ) by A18, A19, FUNCT_1:def_3; x in A /\ U by A20, A21, XBOOLE_0:def_4; hence x in rng q by A23, TARSKI:def_1; ::_thesis: verum end; then A24: card A c= card (G \ AA) by A19, CARD_1:12; card (G \ AA) c= card G by CARD_1:11, XBOOLE_1:36; then card A c= card G by A24, XBOOLE_1:1; hence card A c= C by A15, XBOOLE_1:1; ::_thesis: verum end; end; 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 let iC be infinite Cardinal; ::_thesis: 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 let TM be metrizable TopSpace; ::_thesis: ( ( for Am being Subset of TM st Am is closed & Am is discrete holds card Am c= iC ) implies for Am being Subset of TM st Am is discrete holds card Am c= iC ) assume A1: for Am being Subset of TM st Am is closed & Am is discrete holds card Am c= iC ; ::_thesis: for Am being Subset of TM st Am is discrete holds card Am c= iC let Am be Subset of TM; ::_thesis: ( Am is discrete implies card Am c= iC ) assume A2: Am is discrete ; ::_thesis: card Am c= iC percases ( Am is empty or not Am is empty ) ; suppose Am is empty ; ::_thesis: card Am c= iC hence card Am c= iC ; ::_thesis: verum end; supposeA3: not Am is empty ; ::_thesis: card Am c= iC then reconsider Tm = TM as non empty metrizable TopSpace ; Am c= Cl Am by PRE_TOPC:18; then reconsider ClA = Cl Am as non empty closed Subset of Tm by A3; set TA = Tm | ClA; reconsider A9 = Am as open Subset of (Tm | ClA) by A2, Th12; consider F being countable closed Subset-Family of (Tm | ClA) such that A4: A9 = union F by TOPGEN_4:def_6; consider f being Function of NAT,F such that A5: rng f = F by A3, A4, CARD_3:96, ZFMISC_1:2; A6: for x being set st x in dom f holds card (f . x) c= iC proof let x be set ; ::_thesis: ( x in dom f implies card (f . x) c= iC ) assume x in dom f ; ::_thesis: card (f . x) c= iC then A7: f . x in rng f by FUNCT_1:def_3; then reconsider fx = f . x as Subset of (Tm | ClA) by A5; A8: f . x c= Am by A4, A7, ZFMISC_1:74; then reconsider Fx = f . x as Subset of TM by XBOOLE_1:1; ( [#] (Tm | ClA) = ClA & fx is closed ) by A7, PRE_TOPC:def_5, TOPS_2:def_2; then Fx is closed by TSEP_1:8; hence card (f . x) c= iC by A1, A2, A8, TEX_2:22; ::_thesis: verum end; card (dom f) = omega by A3, A4, CARD_1:47, FUNCT_2:def_1, ZFMISC_1:2; then card (Union f) c= omega *` iC by A6, CARD_2:86; hence card Am c= iC by A4, A5, Lm5; ::_thesis: verum end; end; 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 let C be Cardinal; ::_thesis: 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 let T be TopSpace; ::_thesis: ( ( for A being Subset of T st A is discrete holds card A c= C ) implies 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 ) assume A1: for A being Subset of T st A is discrete holds card A c= C ; ::_thesis: 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 let F be Subset-Family of T; ::_thesis: ( 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 ) implies card F c= C ) assume that A2: F is open and A3: not {} in F and A4: for A, B being Subset of T st A in F & B in F & A <> B holds A misses B ; ::_thesis: card F c= C percases ( F is empty or not F is empty ) ; suppose F is empty ; ::_thesis: card F c= C hence card F c= C ; ::_thesis: verum end; supposeA5: not F is empty ; ::_thesis: card F c= C deffunc H1( set ) -> Element of $1 = the Element of $1; A6: for x being set st x in F holds H1(x) in [#] T proof let x be set ; ::_thesis: ( x in F implies H1(x) in [#] T ) assume A7: x in F ; ::_thesis: H1(x) in [#] T then x <> {} by A3; then H1(x) in x ; hence H1(x) in [#] T by A7; ::_thesis: verum end; consider p being Function of F,([#] T) such that A8: for x being set st x in F holds p . x = H1(x) from FUNCT_2:sch_2(A6); reconsider RNG = rng p as Subset of T ; ex xx being set st xx in F by A5, XBOOLE_0:def_1; then A9: not T is empty by A3; then A10: dom p = F by FUNCT_2:def_1; for x being Point of T st x in RNG holds ex G being Subset of T st ( G is open & RNG /\ G = {x} ) proof let x be Point of T; ::_thesis: ( x in RNG implies ex G being Subset of T st ( G is open & RNG /\ G = {x} ) ) assume A11: x in RNG ; ::_thesis: ex G being Subset of T st ( G is open & RNG /\ G = {x} ) then consider G being set such that A12: G in F and A13: p . G = x by A10, FUNCT_1:def_3; reconsider G = G as Subset of T by A12; A14: RNG /\ G c= {x} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in RNG /\ G or y in {x} ) assume A15: y in RNG /\ G ; ::_thesis: y in {x} then A16: y in G by XBOOLE_0:def_4; y in RNG by A15, XBOOLE_0:def_4; then consider z being set such that A17: z in F and A18: p . z = y by A10, FUNCT_1:def_3; y = H1(z) by A8, A17, A18; then z meets G by A3, A16, A17, XBOOLE_0:3; then x = y by A4, A12, A13, A17, A18; hence y in {x} by TARSKI:def_1; ::_thesis: verum end; take G ; ::_thesis: ( G is open & RNG /\ G = {x} ) thus G is open by A2, A12, TOPS_2:def_1; ::_thesis: RNG /\ G = {x} x = H1(G) by A8, A12, A13; then x in RNG /\ G by A3, A11, A12, XBOOLE_0:def_4; hence RNG /\ G = {x} by A14, ZFMISC_1:33; ::_thesis: verum end; then A19: card RNG c= C by A1, A9, TEX_2:31; for x1, x2 being set st x1 in dom p & x2 in dom p & p . x1 = p . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom p & x2 in dom p & p . x1 = p . x2 implies x1 = x2 ) assume that A20: x1 in dom p and A21: x2 in dom p and A22: p . x1 = p . x2 ; ::_thesis: x1 = x2 A23: ( p . x2 = H1(x2) & x2 <> {} ) by A3, A8, A21; ( p . x1 = H1(x1) & x1 <> {} ) by A3, A8, A20; then x1 meets x2 by A22, A23, XBOOLE_0:3; hence x1 = x2 by A4, A10, A20, A21; ::_thesis: verum end; then p is one-to-one by FUNCT_1:def_4; then card F c= card RNG by A10, CARD_1:10; hence card F c= C by A19, XBOOLE_1:1; ::_thesis: verum end; end; 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 let T be TopSpace; ::_thesis: 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) ) let F be Subset-Family of T; ::_thesis: ( F is Cover of T implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & card G c= card ([#] T) ) ) assume A1: F is Cover of T ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & card G c= card ([#] T) ) percases ( F is empty or not F is empty ) ; supposeA2: F is empty ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & card G c= card ([#] T) ) take F ; ::_thesis: ( F c= F & F is Cover of T & card F c= card ([#] T) ) thus ( F c= F & F is Cover of T & card F c= card ([#] T) ) by A1, A2; ::_thesis: verum end; supposeA3: not F is empty ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & card G c= card ([#] T) ) defpred S1[ set , set ] means $1 in $2; A4: for x being set st x in [#] T holds ex y being set st ( y in F & S1[x,y] ) proof let x be set ; ::_thesis: ( x in [#] T implies ex y being set st ( y in F & S1[x,y] ) ) assume x in [#] T ; ::_thesis: ex y being set st ( y in F & S1[x,y] ) then x in union F by A1, SETFAM_1:45; then ex y being set st ( x in y & y in F ) by TARSKI:def_4; hence ex y being set st ( y in F & S1[x,y] ) ; ::_thesis: verum end; consider g being Function of ([#] T),F such that A5: for x being set st x in [#] T holds S1[x,g . x] from FUNCT_2:sch_1(A4); reconsider R = rng g as Subset-Family of T by XBOOLE_1:1; take R ; ::_thesis: ( R c= F & R is Cover of T & card R c= card ([#] T) ) A6: dom g = [#] T by A3, FUNCT_2:def_1; [#] T c= union R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in union R ) assume x in [#] T ; ::_thesis: x in union R then ( x in g . x & g . x in R ) by A5, A6, FUNCT_1:def_3; hence x in union R by TARSKI:def_4; ::_thesis: verum end; hence ( R c= F & R is Cover of T & card R c= card ([#] T) ) by A6, CARD_1:12, SETFAM_1:def_11; ::_thesis: verum end; end; 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 let TM be metrizable TopSpace; ::_thesis: 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 let iC be infinite Cardinal; ::_thesis: ( ( 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 ) implies density TM c= iC ) assume A1: 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 ; ::_thesis: density TM c= iC percases ( TM is empty or not TM is empty ) ; supposeA2: TM is empty ; ::_thesis: density TM c= iC ex D being Subset of TM st ( D is dense & density TM = card D ) by TOPGEN_1:def_12; hence density TM c= iC by A2; ::_thesis: verum end; supposeA3: not TM is empty ; ::_thesis: density TM c= iC consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that A4: metr is_metric_of the carrier of TM and A5: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def_8; reconsider M = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A3, A4, PCOMPS_1:36; defpred S1[ set , set ] means for n being Nat st $1 = n holds ex G being Subset of TM st ( G = $2 & card G c= iC & ( for p being Element of M ex q being Element of M st ( q in G & dist (p,q) < 1 / (2 |^ n) ) ) ); A6: the carrier of TM = the carrier of M by A3, A4, PCOMPS_2:4; A7: for x being set st x in NAT holds ex y being set st ( y in bool the carrier of TM & S1[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in bool the carrier of TM & S1[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in bool the carrier of TM & S1[x,y] ) then reconsider n = x as Element of NAT ; reconsider r = 1 / (2 |^ n) as Real by XREAL_0:def_1; A8: 2 |^ n > 0 by PREPOWER:6; then consider A being Subset of M such that A9: for p, q being Point of M st p <> q & p in A & q in A holds dist (p,q) >= r and A10: for p being Point of M ex q being Point of M st ( q in A & p in Ball (q,r) ) by COMPL_SP:30; set BALL = { (Ball (p,(r / 2))) where p is Element of M : p in A } ; A11: { (Ball (p,(r / 2))) where p is Element of M : p in A } c= the topology of TM proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Ball (p,(r / 2))) where p is Element of M : p in A } or x in the topology of TM ) assume x in { (Ball (p,(r / 2))) where p is Element of M : p in A } ; ::_thesis: x in the topology of TM then ex p being Point of M st ( x = Ball (p,(r / 2)) & p in A ) ; hence x in the topology of TM by A5, PCOMPS_1:29; ::_thesis: verum end; reconsider BALL = { (Ball (p,(r / 2))) where p is Element of M : p in A } as open Subset-Family of TM by A11, TOPS_2:11, XBOOLE_1:1; defpred S2[ set , set ] means for p being Point of M st Ball (p,(r / 2)) = $1 & p in A holds p = $2; A12: for x being set st x in BALL holds ex y being set st ( y in A & S2[x,y] ) proof let x be set ; ::_thesis: ( x in BALL implies ex y being set st ( y in A & S2[x,y] ) ) assume x in BALL ; ::_thesis: ex y being set st ( y in A & S2[x,y] ) then consider p being Point of M such that A13: x = Ball (p,(r / 2)) and A14: p in A ; A15: r / 2 < r by A8, XREAL_1:216; take p ; ::_thesis: ( p in A & S2[x,p] ) thus p in A by A14; ::_thesis: S2[x,p] let q be Point of M; ::_thesis: ( Ball (q,(r / 2)) = x & q in A implies q = p ) assume that A16: Ball (q,(r / 2)) = x and A17: q in A ; ::_thesis: q = p dist (p,p) = 0 by METRIC_1:1; then p in Ball (p,(r / 2)) by A8, METRIC_1:11; then dist (q,p) < r / 2 by A13, A16, METRIC_1:11; then dist (q,p) < r by A15, XXREAL_0:2; hence q = p by A9, A14, A17; ::_thesis: verum end; consider f being Function of BALL,A such that A18: for x being set st x in BALL holds S2[x,f . x] from FUNCT_2:sch_1(A12); reconsider RNG = rng f as Subset of TM by A6, XBOOLE_1:1; ex q being Point of M st ( q in A & the Point of M in Ball (q,r) ) by A10; then A19: dom f = BALL by FUNCT_2:def_1; then A20: card RNG c= card BALL by CARD_1:12; A21: for A9, B9 being Subset of TM st A9 in BALL & B9 in BALL & A9 <> B9 holds A9 misses B9 proof let A9, B9 be Subset of TM; ::_thesis: ( A9 in BALL & B9 in BALL & A9 <> B9 implies A9 misses B9 ) assume that A22: A9 in BALL and A23: B9 in BALL and A24: A9 <> B9 ; ::_thesis: A9 misses B9 consider b being Element of M such that A25: Ball (b,(r / 2)) = B9 and A26: b in A by A23; consider a being Element of M such that A27: Ball (a,(r / 2)) = A9 and A28: a in A by A22; assume A9 meets B9 ; ::_thesis: contradiction then consider x being set such that A29: x in A9 and A30: x in B9 by XBOOLE_0:3; reconsider x = x as Element of M by A27, A29; A31: dist (a,x) < r / 2 by A27, A29, METRIC_1:11; dist (b,x) < r / 2 by A25, A30, METRIC_1:11; then A32: ( dist (a,b) <= (dist (a,x)) + (dist (x,b)) & (dist (a,x)) + (dist (x,b)) < (r / 2) + (r / 2) ) by A31, METRIC_1:4, XREAL_1:8; dist (a,b) >= r by A9, A24, A25, A26, A27, A28; hence contradiction by A32, XXREAL_0:2; ::_thesis: verum end; take RNG ; ::_thesis: ( RNG in bool the carrier of TM & S1[x,RNG] ) thus RNG in bool the carrier of TM ; ::_thesis: S1[x,RNG] let m be Nat; ::_thesis: ( x = m implies ex G being Subset of TM st ( G = RNG & card G c= iC & ( for p being Element of M ex q being Element of M st ( q in G & dist (p,q) < 1 / (2 |^ m) ) ) ) ) assume A33: x = m ; ::_thesis: ex G being Subset of TM st ( G = RNG & card G c= iC & ( for p being Element of M ex q being Element of M st ( q in G & dist (p,q) < 1 / (2 |^ m) ) ) ) A34: now__::_thesis:_for_p_being_Element_of_M_ex_q_being_Point_of_M_st_ (_q_in_RNG_&_dist_(p,q)_<_1_/_(2_|^_m)_) let p be Element of M; ::_thesis: ex q being Point of M st ( q in RNG & dist (p,q) < 1 / (2 |^ m) ) consider q being Point of M such that A35: q in A and A36: p in Ball (q,r) by A10; take q = q; ::_thesis: ( q in RNG & dist (p,q) < 1 / (2 |^ m) ) A37: Ball (q,(r / 2)) in BALL by A35; then f . (Ball (q,(r / 2))) = q by A18, A35; hence ( q in RNG & dist (p,q) < 1 / (2 |^ m) ) by A19, A33, A36, A37, FUNCT_1:def_3, METRIC_1:11; ::_thesis: verum end; not {} in BALL proof assume {} in BALL ; ::_thesis: contradiction then consider p being Element of M such that A38: Ball (p,(r / 2)) = {} and p in A ; dist (p,p) = 0 by METRIC_1:1; hence contradiction by A8, A38, METRIC_1:11; ::_thesis: verum end; then card BALL c= iC by A1, A21; hence ex G being Subset of TM st ( G = RNG & card G c= iC & ( for p being Element of M ex q being Element of M st ( q in G & dist (p,q) < 1 / (2 |^ m) ) ) ) by A20, A34, XBOOLE_1:1; ::_thesis: verum end; consider p being Function of NAT,(bool the carrier of TM) such that A39: for x being set st x in NAT holds S1[x,p . x] from FUNCT_2:sch_1(A7); reconsider Up = Union p as Subset of TM ; for U being Subset of TM st U <> {} & U is open holds Up meets U proof let U be Subset of TM; ::_thesis: ( U <> {} & U is open implies Up meets U ) reconsider U9 = U as Subset of M by A3, A4, PCOMPS_2:4; assume that A40: U <> {} and A41: U is open ; ::_thesis: Up meets U consider q being set such that A42: q in U by A40, XBOOLE_0:def_1; reconsider q = q as Element of M by A3, A4, A42, PCOMPS_2:4; U9 in Family_open_set M by A5, A41, PRE_TOPC:def_2; then consider r being Real such that A43: r > 0 and A44: Ball (q,r) c= U9 by A42, PCOMPS_1:def_4; consider n being Element of NAT such that A45: 1 / (2 |^ n) <= r by A43, PREPOWER:92; consider G being Subset of TM such that A46: G = p . n and card G c= iC and A47: for p being Element of M ex q being Element of M st ( q in G & dist (p,q) < 1 / (2 |^ n) ) by A39; consider qq being Element of M such that A48: qq in G and A49: dist (q,qq) < 1 / (2 |^ n) by A47; dist (q,qq) < r by A45, A49, XXREAL_0:2; then A50: qq in Ball (q,r) by METRIC_1:11; qq in Up by A46, A48, PROB_1:12; hence Up meets U by A44, A50, XBOOLE_0:3; ::_thesis: verum end; then Up is dense by TOPS_1:45; then A51: density TM c= card Up by TOPGEN_1:def_12; A52: for x being set st x in dom p holds card (p . x) c= iC proof let x be set ; ::_thesis: ( x in dom p implies card (p . x) c= iC ) assume x in dom p ; ::_thesis: card (p . x) c= iC then reconsider n = x as Element of NAT ; ex G being Subset of TM st ( G = p . n & card G c= iC & ( for p being Element of M ex q being Element of M st ( q in G & dist (p,q) < 1 / (2 |^ n) ) ) ) by A39; hence card (p . x) c= iC ; ::_thesis: verum end; card (dom p) = omega by CARD_1:47, FUNCT_2:def_1; then A53: card Up c= omega *` iC by A52, CARD_2:86; omega *` iC = iC by Lm5; hence density TM c= iC by A51, A53, XBOOLE_1:1; ::_thesis: verum end; end; 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 let TM be metrizable TopSpace; ::_thesis: for Am being Subset of TM st Am is dense holds weight TM c= omega *` (card Am) let Am be Subset of TM; ::_thesis: ( Am is dense implies weight TM c= omega *` (card Am) ) assume A1: Am is dense ; ::_thesis: weight TM c= omega *` (card Am) percases ( TM is empty or not TM is empty ) ; suppose TM is empty ; ::_thesis: weight TM c= omega *` (card Am) hence weight TM c= omega *` (card Am) ; ::_thesis: verum end; supposeA2: not TM is empty ; ::_thesis: weight TM c= omega *` (card Am) set TOP = the topology of TM; set cTM = the carrier of TM; consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that A3: metr is_metric_of the carrier of TM and A4: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def_8; reconsider Tm = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A2, A3, PCOMPS_1:36; defpred S1[ set , set ] means for n being Nat st n = $1 holds ( $2 = { (Ball (p,(1 / (2 |^ n)))) where p is Point of Tm : p in Am } & card $2 c= card Am ); A5: for x being set st x in NAT holds ex y being set st ( y in bool the topology of TM & S1[x,y] ) proof defpred S2[ set ] means verum; let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in bool the topology of TM & S1[x,y] ) ) defpred S3[ set ] means $1 in Am; defpred S4[ set ] means ( $1 in Am & S2[$1] ); assume x in NAT ; ::_thesis: ex y being set st ( y in bool the topology of TM & S1[x,y] ) then reconsider n = x as Element of NAT ; deffunc H1( Point of Tm) -> Element of bool the carrier of Tm = Ball ($1,(1 / (2 |^ n))); set BALL1 = { H1(p) where p is Point of Tm : S3[p] } ; set BALL2 = { H1(p) where p is Point of Tm : S4[p] } ; take { H1(p) where p is Point of Tm : S3[p] } ; ::_thesis: ( { H1(p) where p is Point of Tm : S3[p] } in bool the topology of TM & S1[x, { H1(p) where p is Point of Tm : S3[p] } ] ) A6: { H1(p) where p is Point of Tm : S3[p] } c= the topology of TM proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { H1(p) where p is Point of Tm : S3[p] } or y in the topology of TM ) assume y in { H1(p) where p is Point of Tm : S3[p] } ; ::_thesis: y in the topology of TM then ex p being Point of Tm st ( y = H1(p) & S3[p] ) ; hence y in the topology of TM by A4, PCOMPS_1:29; ::_thesis: verum end; A7: for p being Point of Tm holds ( S3[p] iff S4[p] ) ; A8: { H1(p) where p is Point of Tm : S3[p] } = { H1(p) where p is Point of Tm : S4[p] } from FRAENKEL:sch_3(A7); card { H1(p) where p is Point of Tm : S4[p] } c= card Am from BORSUK_2:sch_1(); hence ( { H1(p) where p is Point of Tm : S3[p] } in bool the topology of TM & S1[x, { H1(p) where p is Point of Tm : S3[p] } ] ) by A6, A8; ::_thesis: verum end; consider P being Function of NAT,(bool the topology of TM) such that A9: for x being set st x in NAT holds S1[x,P . x] from FUNCT_2:sch_1(A5); reconsider Up = Union P as Subset-Family of TM by XBOOLE_1:1; A10: for B being Subset of TM st B is open holds for p being Point of TM st p in B holds ex a being Subset of TM st ( a in Up & p in a & a c= B ) proof let B be Subset of TM; ::_thesis: ( B is open implies for p being Point of TM st p in B holds ex a being Subset of TM st ( a in Up & p in a & a c= B ) ) assume B is open ; ::_thesis: for p being Point of TM st p in B holds ex a being Subset of TM st ( a in Up & p in a & a c= B ) then A11: B in the topology of TM by PRE_TOPC:def_2; let p be Point of TM; ::_thesis: ( p in B implies ex a being Subset of TM st ( a in Up & p in a & a c= B ) ) assume A12: p in B ; ::_thesis: ex a being Subset of TM st ( a in Up & p in a & a c= B ) reconsider p9 = p as Point of Tm by A2, A3, PCOMPS_2:4; consider r being Real such that A13: r > 0 and A14: Ball (p9,r) c= B by A4, A11, A12, PCOMPS_1:def_4; consider n being Element of NAT such that A15: 1 / (2 |^ n) <= r / 2 by A13, PREPOWER:92; reconsider B2 = Ball (p9,(1 / (2 |^ n))) as Subset of TM by A2, A3, PCOMPS_2:4; ( 2 |^ n > 0 & dist (p9,p9) = 0 ) by METRIC_1:1, PREPOWER:6; then A16: p9 in B2 by METRIC_1:11; B2 in the topology of TM by A4, PCOMPS_1:29; then B2 is open by PRE_TOPC:def_2; then B2 meets Am by A1, A16, TOPS_1:45; then consider q being set such that A17: q in B2 and A18: q in Am by XBOOLE_0:3; reconsider q = q as Point of Tm by A17; reconsider B3 = Ball (q,(1 / (2 |^ n))) as Subset of TM by A2, A3, PCOMPS_2:4; take B3 ; ::_thesis: ( B3 in Up & p in B3 & B3 c= B ) P . n = { (Ball (t,(1 / (2 |^ n)))) where t is Point of Tm : t in Am } by A9; then B3 in P . n by A18; hence B3 in Up by PROB_1:12; ::_thesis: ( p in B3 & B3 c= B ) A19: dist (p9,q) < 1 / (2 |^ n) by A17, METRIC_1:11; hence p in B3 by METRIC_1:11; ::_thesis: B3 c= B let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B3 or y in B ) assume A20: y in B3 ; ::_thesis: y in B then reconsider t = y as Point of Tm ; dist (q,t) < 1 / (2 |^ n) by A20, METRIC_1:11; then A21: dist (q,t) < r / 2 by A15, XXREAL_0:2; dist (p9,q) < r / 2 by A15, A19, XXREAL_0:2; then ( dist (p9,t) <= (dist (p9,q)) + (dist (q,t)) & (dist (p9,q)) + (dist (q,t)) < (r / 2) + (r / 2) ) by A21, METRIC_1:4, XREAL_1:8; then dist (p9,t) < r by XXREAL_0:2; then t in Ball (p9,r) by METRIC_1:11; hence y in B by A14; ::_thesis: verum end; Up is Basis of TM by A10, YELLOW_9:32; then A22: weight TM c= card Up by WAYBEL23:73; A23: card (dom P) = omega by CARD_1:47, FUNCT_2:def_1; for x being set st x in dom P holds card (P . x) c= card Am by A9; then card (Union P) c= omega *` (card Am) by A23, CARD_2:86; hence weight TM c= omega *` (card Am) by A22, XBOOLE_1:1; ::_thesis: verum end; end; end; Lm7: for TM being metrizable TopSpace for iC being infinite Cardinal st density TM c= iC holds weight TM c= iC proof let TM be metrizable TopSpace; ::_thesis: for iC being infinite Cardinal st density TM c= iC holds weight TM c= iC let iC be infinite Cardinal; ::_thesis: ( density TM c= iC implies weight TM c= iC ) consider A being Subset of TM such that A1: A is dense and A2: density TM = card A by TOPGEN_1:def_12; A3: weight TM c= omega *` (card A) by A1, Th17; assume density TM c= iC ; ::_thesis: weight TM c= iC then omega *` (card A) c= omega *` iC by A2, CARD_2:90; then weight TM c= omega *` iC by A3, XBOOLE_1:1; hence weight TM c= iC by Lm5; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: 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 ) ) let iC be infinite Cardinal; ::_thesis: ( 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 ) ) hereby ::_thesis: ( ( 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 ) ) implies weight TM c= iC ) assume A1: weight TM c= iC ; ::_thesis: for F being Subset-Family of TM st F is open & F is Cover of TM holds ex G being Subset-Family of TM st ( b3 c= G & b3 is Cover of TM & card b3 c= iC ) let F be Subset-Family of TM; ::_thesis: ( F is open & F is Cover of TM implies ex G being Subset-Family of TM st ( b2 c= G & b2 is Cover of TM & card b2 c= iC ) ) assume that A2: F is open and A3: F is Cover of TM ; ::_thesis: ex G being Subset-Family of TM st ( b2 c= G & b2 is Cover of TM & card b2 c= iC ) percases ( TM is empty or not TM is empty ) ; supposeA4: TM is empty ; ::_thesis: ex G being Subset-Family of TM st ( b2 c= G & b2 is Cover of TM & card b2 c= iC ) reconsider G = {} as Subset-Family of TM by TOPGEN_4:18; take G = G; ::_thesis: ( G c= F & G is Cover of TM & card G c= iC ) the carrier of TM = {} by A4; then [#] TM = union G ; hence ( G c= F & G is Cover of TM & card G c= iC ) by SETFAM_1:def_11, XBOOLE_1:2; ::_thesis: verum end; suppose not TM is empty ; ::_thesis: ex G being Subset-Family of TM st ( b2 c= G & b2 is Cover of TM & card b2 c= iC ) then consider G being open Subset-Family of TM such that A5: ( G c= F & union G = union F & card G c= weight TM ) by A2, TOPGEN_2:11; reconsider G = G as Subset-Family of TM ; take G = G; ::_thesis: ( G c= F & G is Cover of TM & card G c= iC ) union F = [#] TM by A3, SETFAM_1:45; hence ( G c= F & G is Cover of TM & card G c= iC ) by A1, A5, SETFAM_1:def_11, XBOOLE_1:1; ::_thesis: verum end; end; end; assume for F being Subset-Family of TM st F is open & F is Cover of TM holds ex G being Subset-Family of TM st ( G c= F & G is Cover of TM & card G c= iC ) ; ::_thesis: weight TM c= iC then for A being Subset of TM st A is closed & A is discrete holds card A c= iC by Th13; then for A being Subset of TM st A is discrete holds card A c= iC by Th14; then for F being Subset-Family of TM st F is open & not {} in F & ( for A, B being Subset of TM st A in F & B in F & A <> B holds A misses B ) holds card F c= iC by Th15; then density TM c= iC by Lm6; hence weight TM c= iC by Lm7; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: 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 ) let iC be infinite Cardinal; ::_thesis: ( weight TM c= iC iff for Am being Subset of TM st Am is closed & Am is discrete holds card Am c= iC ) hereby ::_thesis: ( ( for Am being Subset of TM st Am is closed & Am is discrete holds card Am c= iC ) implies weight TM c= iC ) assume weight TM c= iC ; ::_thesis: for Am being Subset of TM st Am is closed & Am is discrete holds card Am c= iC then 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 ) by Th18; hence for Am being Subset of TM st Am is closed & Am is discrete holds card Am c= iC by Th13; ::_thesis: verum end; assume for Am being Subset of TM st Am is closed & Am is discrete holds card Am c= iC ; ::_thesis: weight TM c= iC then for Am being Subset of TM st Am is discrete holds card Am c= iC by Th14; then 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 by Th15; then density TM c= iC by Lm6; hence weight TM c= iC by Lm7; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: 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 ) let iC be infinite Cardinal; ::_thesis: ( weight TM c= iC iff for Am being Subset of TM st Am is discrete holds card Am c= iC ) hereby ::_thesis: ( ( for Am being Subset of TM st Am is discrete holds card Am c= iC ) implies weight TM c= iC ) assume weight TM c= iC ; ::_thesis: for A being Subset of TM st A is discrete holds card A c= iC then for A being Subset of TM st A is closed & A is discrete holds card A c= iC by Th19; hence for A being Subset of TM st A is discrete holds card A c= iC by Th14; ::_thesis: verum end; assume for A being Subset of TM st A is discrete holds card A c= iC ; ::_thesis: weight TM c= iC then for F being Subset-Family of TM st F is open & not {} in F & ( for A, B being Subset of TM st A in F & B in F & A <> B holds A misses B ) holds card F c= iC by Th15; then density TM c= iC by Lm6; hence weight TM c= iC by Lm7; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: 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 ) let iC be infinite Cardinal; ::_thesis: ( 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 ) hereby ::_thesis: ( ( 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 ) implies weight TM c= iC ) assume weight TM c= iC ; ::_thesis: for F being Subset-Family of TM st F is open & not {} in F & ( for A, B being Subset of TM st A in F & B in F & A <> B holds A misses B ) holds card F c= iC then for A being Subset of TM st A is discrete holds card A c= iC by Th20; hence for F being Subset-Family of TM st F is open & not {} in F & ( for A, B being Subset of TM st A in F & B in F & A <> B holds A misses B ) holds card F c= iC by Th15; ::_thesis: verum end; assume for F being Subset-Family of TM st F is open & not {} in F & ( for A, B being Subset of TM st A in F & B in F & A <> B holds A misses B ) holds card F c= iC ; ::_thesis: weight TM c= iC then density TM c= iC by Lm6; hence weight TM c= iC by Lm7; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: for iC being infinite Cardinal holds ( weight TM c= iC iff density TM c= iC ) let iC be infinite Cardinal; ::_thesis: ( weight TM c= iC iff density TM c= iC ) consider A being Subset of TM such that A1: A is dense and A2: density TM = card A by TOPGEN_1:def_12; hereby ::_thesis: ( density TM c= iC implies weight TM c= iC ) assume weight TM c= iC ; ::_thesis: density TM c= iC then for F being Subset-Family of TM st F is open & not {} in F & ( for A, B being Subset of TM st A in F & B in F & A <> B holds A misses B ) holds card F c= iC by Th21; hence density TM c= iC by Lm6; ::_thesis: verum end; A3: weight TM c= omega *` (card A) by A1, Th17; assume density TM c= iC ; ::_thesis: weight TM c= iC then omega *` (card A) c= omega *` iC by A2, CARD_2:90; then weight TM c= omega *` iC by A3, XBOOLE_1:1; hence weight TM c= iC by Lm5; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: 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 ) let iC be infinite Cardinal; ::_thesis: 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 ) let B be Basis of TM; ::_thesis: ( ( 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 ) ) implies ex underB being Basis of TM st ( underB c= B & card underB c= iC ) ) assume A1: for F being Subset-Family of TM st F is open & F is Cover of TM holds ex G being Subset-Family of TM st ( G c= F & G is Cover of TM & card G c= iC ) ; ::_thesis: ex underB being Basis of TM st ( underB c= B & card underB c= iC ) percases ( TM is empty or not TM is empty ) ; suppose TM is empty ; ::_thesis: ex underB being Basis of TM st ( underB c= B & card underB c= iC ) then weight TM = 0 ; then consider underB being Basis of TM such that A2: card underB = 0 by WAYBEL23:74; take underB ; ::_thesis: ( underB c= B & card underB c= iC ) underB = {} by A2; hence ( underB c= B & card underB c= iC ) by XBOOLE_1:2; ::_thesis: verum end; supposeA3: not TM is empty ; ::_thesis: ex underB being Basis of TM st ( underB c= B & card underB c= iC ) set TOP = the topology of TM; set cT = the carrier of TM; consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that A4: metr is_metric_of the carrier of TM and A5: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def_8; reconsider Tm = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A3, A4, PCOMPS_1:36; defpred S1[ set , set ] means for n being Nat st $1 = n holds ex G being open Subset-Family of TM st ( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } & G is Cover of TM & card G c= iC & $2 = G ); A6: B c= the topology of TM by TOPS_2:64; A7: for x being set st x in NAT holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S1[x,y] then reconsider n = x as Nat ; set F = { U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } ; A8: { U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } c= the topology of TM proof let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in { U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } or f in the topology of TM ) assume f in { U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } ; ::_thesis: f in the topology of TM then ex U being Subset of TM st ( f = U & U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) ; hence f in the topology of TM by A6; ::_thesis: verum end; then reconsider F = { U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } as Subset-Family of TM by XBOOLE_1:1; reconsider F = F as open Subset-Family of TM by A8, TOPS_2:11; the carrier of TM c= union F proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of TM or y in union F ) assume A9: y in the carrier of TM ; ::_thesis: y in union F then reconsider p = y as Point of TM ; reconsider q = y as Element of Tm by A3, A4, A9, PCOMPS_2:4; ( 2 |^ n > 0 & dist (q,q) = 0 ) by METRIC_1:1, NEWTON:83; then A10: q in Ball (q,(1 / (2 |^ n))) by METRIC_1:11; reconsider BALL = Ball (q,(1 / (2 |^ n))) as Subset of TM by A3, A4, PCOMPS_2:4; BALL in Family_open_set Tm by PCOMPS_1:29; then BALL is open by A5, PRE_TOPC:def_2; then consider U being Subset of TM such that A11: U in B and A12: p in U and A13: U c= BALL by A10, YELLOW_9:31; U in F by A11, A13; hence y in union F by A12, TARSKI:def_4; ::_thesis: verum end; then F is Cover of TM by SETFAM_1:def_11; then consider G being Subset-Family of TM such that A14: G c= F and A15: ( G is Cover of TM & card G c= iC ) by A1; take G ; ::_thesis: S1[x,G] let m be Nat; ::_thesis: ( x = m implies ex G being open Subset-Family of TM st ( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ m))) ) } & G is Cover of TM & card G c= iC & G = G ) ) assume A16: x = m ; ::_thesis: ex G being open Subset-Family of TM st ( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ m))) ) } & G is Cover of TM & card G c= iC & G = G ) G is open by A14, TOPS_2:11; hence ex G being open Subset-Family of TM st ( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ m))) ) } & G is Cover of TM & card G c= iC & G = G ) by A14, A15, A16; ::_thesis: verum end; consider f being Function such that A17: ( dom f = NAT & ( for e being set st e in NAT holds S1[e,f . e] ) ) from CLASSES1:sch_1(A7); A18: union (rng f) c= B proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in union (rng f) or b in B ) assume b in union (rng f) ; ::_thesis: b in B then consider y being set such that A19: b in y and A20: y in rng f by TARSKI:def_4; consider x being set such that A21: x in dom f and A22: f . x = y by A20, FUNCT_1:def_3; reconsider n = x as Nat by A17, A21; ex G being open Subset-Family of TM st ( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } & G is Cover of TM & card G c= iC & f . n = G ) by A17, A21; then b in { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } by A19, A22; then ex U being Subset of TM st ( U = b & U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) ; hence b in B ; ::_thesis: verum end; then reconsider Urngf = union (rng f) as Subset-Family of TM by XBOOLE_1:1; for A being Subset of TM st A is open holds for p being Point of TM st p in A holds ex a being Subset of TM st ( a in Urngf & p in a & a c= A ) proof let A be Subset of TM; ::_thesis: ( A is open implies for p being Point of TM st p in A holds ex a being Subset of TM st ( a in Urngf & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of TM st p in A holds ex a being Subset of TM st ( a in Urngf & p in a & a c= A ) then A23: A in Family_open_set Tm by A5, PRE_TOPC:def_2; let p be Point of TM; ::_thesis: ( p in A implies ex a being Subset of TM st ( a in Urngf & p in a & a c= A ) ) assume A24: p in A ; ::_thesis: ex a being Subset of TM st ( a in Urngf & p in a & a c= A ) reconsider p9 = p as Element of Tm by A3, A4, PCOMPS_2:4; consider r being Real such that A25: r > 0 and A26: Ball (p9,r) c= A by A23, A24, PCOMPS_1:def_4; consider n being Element of NAT such that A27: 1 / (2 |^ n) <= r / 2 by A25, PREPOWER:92; consider G being open Subset-Family of TM such that A28: G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } and A29: G is Cover of TM and card G c= iC and A30: f . n = G by A17; [#] TM = union G by A29, SETFAM_1:45; then consider a being set such that A31: p in a and A32: a in G by A3, TARSKI:def_4; a in { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } by A28, A32; then consider U being Subset of TM such that A33: a = U and U in B and A34: ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ; take U ; ::_thesis: ( U in Urngf & p in U & U c= A ) f . n in rng f by A17, FUNCT_1:def_3; hence ( U in Urngf & p in U ) by A30, A31, A32, A33, TARSKI:def_4; ::_thesis: U c= A thus U c= A ::_thesis: verum proof let u9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u9 in U or u9 in A ) consider pp being Element of Tm such that A35: U c= Ball (pp,(1 / (2 |^ n))) by A34; assume A36: u9 in U ; ::_thesis: u9 in A then reconsider u = u9 as Element of Tm by A3, A4, PCOMPS_2:4; dist (pp,u) < 1 / (2 |^ n) by A35, A36, METRIC_1:11; then A37: dist (pp,u) < r / 2 by A27, XXREAL_0:2; dist (pp,p9) < 1 / (2 |^ n) by A31, A33, A35, METRIC_1:11; then dist (p9,pp) < r / 2 by A27, XXREAL_0:2; then ( dist (p9,u) <= (dist (p9,pp)) + (dist (pp,u)) & (dist (p9,pp)) + (dist (pp,u)) < (r / 2) + (r / 2) ) by A37, METRIC_1:4, XREAL_1:8; then dist (p9,u) < (r / 2) + (r / 2) by XXREAL_0:2; then u in Ball (p9,r) by METRIC_1:11; hence u9 in A by A26; ::_thesis: verum end; end; then reconsider Urngf = Urngf as Basis of TM by A6, A18, XBOOLE_1:1, YELLOW_9:32; take Urngf ; ::_thesis: ( Urngf c= B & card Urngf c= iC ) for x being set st x in dom f holds card (f . x) c= iC proof let x be set ; ::_thesis: ( x in dom f implies card (f . x) c= iC ) assume x in dom f ; ::_thesis: card (f . x) c= iC then reconsider n = x as Element of NAT by A17; ex G being open Subset-Family of TM st ( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball (p,(1 / (2 |^ n))) ) } & G is Cover of TM & card G c= iC & f . n = G ) by A17; hence card (f . x) c= iC ; ::_thesis: verum end; then card (Union f) c= omega *` iC by A17, CARD_1:47, CARD_2:86; hence ( Urngf c= B & card Urngf c= iC ) by A18, Lm5; ::_thesis: verum end; end; end; 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 ) ) proof let T be TopSpace; ::_thesis: ( 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 ) ) hereby ::_thesis: ( ( 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 ) ) implies T is Lindelof ) assume A1: T is Lindelof ; ::_thesis: 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 ) let F be Subset-Family of T; ::_thesis: ( F is open & F is Cover of T implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & card G c= omega ) ) assume ( F is open & F is Cover of T ) ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & card G c= omega ) then consider G being Subset-Family of T such that A2: ( G c= F & G is Cover of T & G is countable ) by A1, Def2; take G = G; ::_thesis: ( G c= F & G is Cover of T & card G c= omega ) thus ( G c= F & G is Cover of T & card G c= omega ) by A2, CARD_3:def_14; ::_thesis: verum end; assume A3: 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 ) ; ::_thesis: T is Lindelof let F be Subset-Family of T; :: according to METRIZTS:def_2 ::_thesis: ( F is open & F is Cover of T implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) ) assume ( F is open & F is Cover of T ) ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) then consider G being Subset-Family of T such that A4: ( G c= F & G is Cover of T ) and A5: card G c= omega by A3; G is countable by A5, CARD_3:def_14; hence ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) by A4; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: for B being Basis of TM st TM is Lindelof holds ex B9 being Basis of TM st ( B9 c= B & B9 is countable ) let B be Basis of TM; ::_thesis: ( TM is Lindelof implies ex B9 being Basis of TM st ( B9 c= B & B9 is countable ) ) assume TM is Lindelof ; ::_thesis: ex B9 being Basis of TM st ( B9 c= B & B9 is countable ) then for F being Subset-Family of TM st F is open & F is Cover of TM holds ex G being Subset-Family of TM st ( G c= F & G is Cover of TM & card G c= omega ) by Lm8; then consider underB being Basis of TM such that A1: ( underB c= B & card underB c= omega ) by Th23; take underB ; ::_thesis: ( underB c= B & underB is countable ) thus ( underB c= B & underB is countable ) by A1, CARD_3:def_14; ::_thesis: verum end; Lm9: for TM being metrizable TopSpace holds ( TM is Lindelof iff TM is second-countable ) proof let TM be metrizable TopSpace; ::_thesis: ( TM is Lindelof iff TM is second-countable ) hereby ::_thesis: ( TM is second-countable implies TM is Lindelof ) assume TM is Lindelof ; ::_thesis: TM is second-countable then for F being Subset-Family of TM st F is open & F is Cover of TM holds ex G being Subset-Family of TM st ( G c= F & G is Cover of TM & card G c= omega ) by Lm8; then weight TM c= omega by Th18; hence TM is second-countable by WAYBEL23:def_6; ::_thesis: verum end; assume TM is second-countable ; ::_thesis: TM is Lindelof then weight TM c= omega by WAYBEL23:def_6; then for F being Subset-Family of TM st F is open & F is Cover of TM holds ex G being Subset-Family of TM st ( G c= F & G is Cover of TM & card G c= omega ) by Th18; hence TM is Lindelof by Lm8; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: ( TM is Lindelof iff TM is separable ) hereby ::_thesis: ( TM is separable implies TM is Lindelof ) assume TM is Lindelof ; ::_thesis: TM is separable then weight TM c= omega by WAYBEL23:def_6; then density TM c= omega by Th22; hence TM is separable by TOPGEN_1:def_13; ::_thesis: verum end; assume TM is separable ; ::_thesis: TM is Lindelof then density TM c= omega by TOPGEN_1:def_13; then weight TM c= omega by Th22; then TM is second-countable by WAYBEL23:def_6; hence TM is Lindelof by Lm9; ::_thesis: verum 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 set X = the non empty finite set ; TopSpaceMetr (DiscreteSpace the non empty finite set ) is finite ; hence ex b1 being non empty TopSpace st ( b1 is Lindelof & b1 is metrizable ) ; ::_thesis: verum end; cluster TopSpace-like second-countable -> Lindelof for TopStruct ; coherence for b1 being TopSpace st b1 is second-countable holds b1 is Lindelof proof let T be TopSpace; ::_thesis: ( T is second-countable implies T is Lindelof ) assume A1: T is second-countable ; ::_thesis: T is Lindelof let F be Subset-Family of T; :: according to METRIZTS:def_2 ::_thesis: ( F is open & F is Cover of T implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) ) assume that A2: F is open and A3: F is Cover of T ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) percases ( T is empty or not T is empty ) ; supposeA4: T is empty ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) take F ; ::_thesis: ( F c= F & F is Cover of T & F is countable ) F c= {{}} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in {{}} ) assume x in F ; ::_thesis: x in {{}} then x = {} by A4; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; hence ( F c= F & F is Cover of T & F is countable ) by A3; ::_thesis: verum end; suppose not T is empty ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) hence ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) by A1, A2, A3, COMPL_SP:34; ::_thesis: verum end; end; 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 let T be TopSpace; ::_thesis: ( T is regular & T is Lindelof implies T is normal ) assume that A5: T is regular and A6: T is Lindelof ; ::_thesis: T is normal percases ( T is empty or not T is empty ) ; supposeA7: T is empty ; ::_thesis: T is normal let F1, F2 be Subset of T; :: according to PRE_TOPC:def_12 ::_thesis: ( not F1 is closed or not F2 is closed or not F1 misses F2 or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) ) assume that F1 is closed and F2 is closed and A8: F1 misses F2 ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) take F1 ; ::_thesis: ex b1 being Element of bool the carrier of T st ( F1 is open & b1 is open & F1 c= F1 & F2 c= b1 & F1 misses b1 ) take F2 ; ::_thesis: ( F1 is open & F2 is open & F1 c= F1 & F2 c= F2 & F1 misses F2 ) thus ( F1 is open & F2 is open & F1 c= F1 & F2 c= F2 & F1 misses F2 ) by A7, A8; ::_thesis: verum end; supposeA9: not T is empty ; ::_thesis: T is normal set TOP = the topology of T; for A being Subset of T for U being open Subset of T st A is closed & U is open & A c= U holds ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) proof let A be Subset of T; ::_thesis: for U being open Subset of T st A is closed & U is open & A c= U holds ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) let U be open Subset of T; ::_thesis: ( A is closed & U is open & A c= U implies ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) ) assume that A10: A is closed and U is open and A11: A c= U ; ::_thesis: ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) defpred S1[ set , set ] means for p being Point of T st p = c1 holds ex W being Subset of T st ( W is open & p in W & Cl W c= U & c2 = W ); A12: for x being set st x in A holds ex y being set st ( y in the topology of T & S1[x,y] ) proof let x be set ; ::_thesis: ( x in A implies ex y being set st ( y in the topology of T & S1[x,y] ) ) assume A13: x in A ; ::_thesis: ex y being set st ( y in the topology of T & S1[x,y] ) then reconsider p = x as Point of T ; U = (U `) ` ; then consider G1, G2 being Subset of T such that A14: G1 is open and A15: G2 is open and A16: p in G1 and A17: U ` c= G2 and A18: G1 misses G2 by A5, A11, A13, PRE_TOPC:def_11; A19: ( Cl (G2 `) = G2 ` & G2 ` c= U ) by A15, A17, PRE_TOPC:22, SUBSET_1:17; take G1 ; ::_thesis: ( G1 in the topology of T & S1[x,G1] ) thus G1 in the topology of T by A14, PRE_TOPC:def_2; ::_thesis: S1[x,G1] G1 c= G2 ` by A18, SUBSET_1:23; then A20: Cl G1 c= Cl (G2 `) by PRE_TOPC:19; let q be Point of T; ::_thesis: ( q = x implies ex W being Subset of T st ( W is open & q in W & Cl W c= U & G1 = W ) ) assume q = x ; ::_thesis: ex W being Subset of T st ( W is open & q in W & Cl W c= U & G1 = W ) hence ex W being Subset of T st ( W is open & q in W & Cl W c= U & G1 = W ) by A14, A16, A20, A19, XBOOLE_1:1; ::_thesis: verum end; consider w being Function of A, the topology of T such that A21: for x being set st x in A holds S1[x,w . x] from FUNCT_2:sch_1(A12); A ` in the topology of T by A10, PRE_TOPC:def_2; then ( the topology of T is open & {(A `)} c= the topology of T ) by ZFMISC_1:31; then reconsider RNG = rng w, AA = {(A `)} as open Subset-Family of T by TOPS_2:11, XBOOLE_1:1; set RngA = RNG \/ AA; A22: dom w = A by FUNCT_2:def_1; [#] T c= union (RNG \/ AA) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in union (RNG \/ AA) ) assume A23: x in [#] T ; ::_thesis: x in union (RNG \/ AA) percases ( x in A or not x in A ) ; supposeA24: x in A ; ::_thesis: x in union (RNG \/ AA) then consider W being Subset of T such that W is open and A25: x in W and Cl W c= U and A26: w . x = W by A21; W in rng w by A22, A24, A26, FUNCT_1:def_3; then W in RNG \/ AA by XBOOLE_0:def_3; hence x in union (RNG \/ AA) by A25, TARSKI:def_4; ::_thesis: verum end; supposeA27: not x in A ; ::_thesis: x in union (RNG \/ AA) A ` in AA by TARSKI:def_1; then A28: A ` in RNG \/ AA by XBOOLE_0:def_3; x in A ` by A23, A27, XBOOLE_0:def_5; hence x in union (RNG \/ AA) by A28, TARSKI:def_4; ::_thesis: verum end; end; end; then ( RNG \/ AA is open Subset-Family of T & RNG \/ AA is Cover of T ) by SETFAM_1:def_11, TOPS_2:13; then consider G being Subset-Family of T such that A29: G c= RNG \/ AA and A30: G is Cover of T and A31: G is countable by A6, Def2; A32: [#] T = union G by A30, SETFAM_1:45; percases ( G \ AA is empty or not G \ AA is empty ) ; suppose G \ AA is empty ; ::_thesis: ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) then G c= AA by XBOOLE_1:37; then A33: union G c= union AA by ZFMISC_1:77; take W = NAT --> ({} T); ::_thesis: ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) rng W = {({} T)} by FUNCOP_1:8; then A34: ( ({} T) ` = [#] T & Union W = {} T ) by ZFMISC_1:25; union AA = A ` by ZFMISC_1:25; then A ` = [#] T by A32, A33, XBOOLE_0:def_10; hence ( A c= Union W & Union W c= U ) by A34, SUBSET_1:42, XBOOLE_1:2; ::_thesis: for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) let n be Element of NAT ; ::_thesis: ( Cl (W . n) c= U & W . n is open ) W . n = {} T by FUNCOP_1:7; then Cl (W . n) = {} T by PRE_TOPC:22; hence ( Cl (W . n) c= U & W . n is open ) by FUNCOP_1:7, XBOOLE_1:2; ::_thesis: verum end; supposeA35: not G \ AA is empty ; ::_thesis: ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) G \ AA is countable by A31, CARD_3:95; then consider W being Function of NAT,(G \ AA) such that A36: rng W = G \ AA by A35, CARD_3:96; reconsider W = W as Function of NAT,(bool the carrier of T) by A35, A36, FUNCT_2:6; take W ; ::_thesis: ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) thus A c= Union W ::_thesis: ( Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Union W ) assume A37: x in A ; ::_thesis: x in Union W then consider y being set such that A38: x in y and A39: y in G by A32, TARSKI:def_4; not x in A ` by A37, XBOOLE_0:def_5; then not y in AA by A38, TARSKI:def_1; then y in rng W by A36, A39, XBOOLE_0:def_5; then ex n being set st ( n in dom W & W . n = y ) by FUNCT_1:def_3; hence x in Union W by A38, PROB_1:12; ::_thesis: verum end; A40: dom W = NAT by FUNCT_2:def_1; thus Union W c= U ::_thesis: for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union W or x in U ) assume x in Union W ; ::_thesis: x in U then consider n being Element of NAT such that A41: x in W . n by PROB_1:12; A42: W . n in G \ AA by A36, A40, FUNCT_1:def_3; then W . n in G by ZFMISC_1:56; then A43: ( W . n in RNG or W . n in AA ) by A29, XBOOLE_0:def_3; W . n <> A ` by A42, ZFMISC_1:56; then consider xx being set such that A44: ( xx in dom w & w . xx = W . n ) by A43, FUNCT_1:def_3, TARSKI:def_1; consider W9 being Subset of T such that W9 is open and xx in W9 and A45: Cl W9 c= U and A46: W . n = W9 by A21, A22, A44; W9 c= Cl W9 by PRE_TOPC:18; then x in Cl W9 by A41, A46; hence x in U by A45; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ( Cl (W . n) c= U & W . n is open ) A47: W . n in G \ AA by A36, A40, FUNCT_1:def_3; then W . n in G by ZFMISC_1:56; then A48: ( W . n in RNG or W . n in AA ) by A29, XBOOLE_0:def_3; W . n <> A ` by A47, ZFMISC_1:56; then consider xx being set such that A49: ( xx in dom w & w . xx = W . n ) by A48, FUNCT_1:def_3, TARSKI:def_1; ex W9 being Subset of T st ( W9 is open & xx in W9 & Cl W9 c= U & W . n = W9 ) by A21, A22, A49; hence ( Cl (W . n) c= U & W . n is open ) ; ::_thesis: verum end; end; end; hence T is normal by A9, NAGATA_1:18; ::_thesis: verum end; end; end; cluster TopSpace-like countable -> Lindelof for TopStruct ; coherence for b1 being TopSpace st b1 is countable holds b1 is Lindelof proof let T be TopSpace; ::_thesis: ( T is countable implies T is Lindelof ) assume T is countable ; ::_thesis: T is Lindelof then [#] T is countable by ORDERS_4:def_2; then A50: card ([#] T) c= omega by CARD_3:def_14; let F be Subset-Family of T; :: according to METRIZTS:def_2 ::_thesis: ( F is open & F is Cover of T implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) ) assume that F is open and A51: F is Cover of T ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is countable ) consider G being Subset-Family of T such that A52: ( G c= F & G is Cover of T ) and A53: card G c= card ([#] T) by A51, Th16; take G ; ::_thesis: ( G c= F & G is Cover of T & G is countable ) card G c= omega by A50, A53, XBOOLE_1:1; hence ( G c= F & G is Cover of T & G is countable ) by A52, CARD_3:def_14; ::_thesis: verum end; end; Lm11: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is second-countable proof reconsider R = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17; ( TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) & TopStruct(# the carrier of (TOP-REAL (1 + 1)), the topology of (TOP-REAL (1 + 1)) #) = TopSpaceMetr (Euclid (1 + 1)) ) by EUCLID:def_8; then A1: weight [:TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] = weight TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by Th4, TOPREAL7:25; Cl R = [#] R^1 by BORSUK_5:15; then R is dense by TOPS_1:def_3; then R^1 is separable by TOPGEN_4:6; then A2: weight [:R^1,R^1:] c= omega by TOPMETR:def_6, WAYBEL23:def_6; TopStruct(# the carrier of [:R^1,R^1:], the topology of [:R^1,R^1:] #), TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) are_homeomorphic by TOPREAL6:77, TOPREALA:15; then A3: weight TopStruct(# the carrier of [:R^1,R^1:], the topology of [:R^1,R^1:] #) = weight TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by Th4; weight TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) c= weight [:TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] by Th6; then weight TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) c= omega by A1, A3, A2, XBOOLE_1:1; hence TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is second-countable by WAYBEL23:def_6; ::_thesis: verum 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 defpred S1[ Nat] means TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is second-countable ; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) A2: ( TopStruct(# the carrier of (TOP-REAL (n + 1)), the topology of (TOP-REAL (n + 1)) #) = TopSpaceMetr (Euclid (n + 1)) & n in NAT ) by EUCLID:def_8, ORDINAL1:def_12; assume S1[n] ; ::_thesis: S1[n + 1] then A3: weight [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] c= omega by Lm11, WAYBEL23:def_6; ( TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) & TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) ) by EUCLID:def_8; then weight [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] = weight TopStruct(# the carrier of (TOP-REAL (n + 1)), the topology of (TOP-REAL (n + 1)) #) by A2, Th4, TOPREAL7:25; hence S1[n + 1] by A3, WAYBEL23:def_6; ::_thesis: verum end; [#] (TOP-REAL 0) = REAL 0 by EUCLID:22 .= 0 -tuples_on REAL by EUCLID:def_1 .= {(<*> REAL)} by FINSEQ_2:94 ; then TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) is finite ; then A4: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1); hence TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is second-countable ; ::_thesis: verum end; end; registration let T be Lindelof TopSpace; let A be closed Subset of T; clusterT | A -> Lindelof ; coherence T | A is Lindelof proof reconsider E = {{}} as Subset-Family of (T | A) by SETFAM_1:46; defpred S1[ set , set ] means A /\ A = T; set TOP = the topology of T; let FA be Subset-Family of (T | A); :: according to METRIZTS:def_2 ::_thesis: ( FA is open & FA is Cover of (T | A) implies ex G being Subset-Family of (T | A) st ( G c= FA & G is Cover of (T | A) & G is countable ) ) assume that A1: FA is open and A2: FA is Cover of (T | A) ; ::_thesis: ex G being Subset-Family of (T | A) st ( G c= FA & G is Cover of (T | A) & G is countable ) A3: for x being set st x in FA holds ex y being set st ( y in the topology of T & S1[x,y] ) proof let x be set ; ::_thesis: ( x in FA implies ex y being set st ( y in the topology of T & S1[x,y] ) ) assume A4: x in FA ; ::_thesis: ex y being set st ( y in the topology of T & S1[x,y] ) reconsider X = x as Subset of (T | A) by A4; X is open by A1, A4, TOPS_2:def_1; then X in the topology of (T | A) by PRE_TOPC:def_2; then consider Q being Subset of T such that A5: ( Q in the topology of T & X = Q /\ ([#] (T | A)) ) by PRE_TOPC:def_4; take Q ; ::_thesis: ( Q in the topology of T & S1[x,Q] ) thus ( Q in the topology of T & S1[x,Q] ) by A5, PRE_TOPC:def_5; ::_thesis: verum end; consider f being Function of FA, the topology of T such that A6: for x being set st x in FA holds S1[x,f . x] from FUNCT_2:sch_1(A3); A ` in the topology of T by PRE_TOPC:def_2; then ( the topology of T is open & {(A `)} c= the topology of T ) by ZFMISC_1:31; then reconsider RNG = rng f, AA = {(A `)} as open Subset-Family of T by TOPS_2:11, XBOOLE_1:1; reconsider RA = RNG \/ AA as open Subset-Family of T by TOPS_2:13; A7: A = [#] (T | A) by PRE_TOPC:def_5; A8: dom f = FA by FUNCT_2:def_1; [#] T c= union RA proof A9: A \/ (A `) = [#] the carrier of T by SUBSET_1:10; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in union RA ) assume A10: x in [#] T ; ::_thesis: x in union RA percases ( x in A or x in A ` ) by A9, A10, XBOOLE_0:def_3; supposeA11: x in A ; ::_thesis: x in union RA A = union FA by A2, A7, SETFAM_1:45; then consider y being set such that A12: x in y and A13: y in FA by A11, TARSKI:def_4; f . y in RNG by A8, A13, FUNCT_1:def_3; then A14: f . y in RA by XBOOLE_0:def_3; (f . y) /\ A = y by A6, A13; then x in f . y by A12, XBOOLE_0:def_4; hence x in union RA by A14, TARSKI:def_4; ::_thesis: verum end; supposeA15: x in A ` ; ::_thesis: x in union RA A ` in AA by TARSKI:def_1; then A ` in RA by XBOOLE_0:def_3; hence x in union RA by A15, TARSKI:def_4; ::_thesis: verum end; end; end; then RA is Cover of T by SETFAM_1:def_11; then consider G being Subset-Family of T such that A16: G c= RA and A17: G is Cover of T and A18: G is countable by Def2; set GA = G | A; take GE = (G | A) \ E; ::_thesis: ( GE c= FA & GE is Cover of (T | A) & GE is countable ) thus GE c= FA ::_thesis: ( GE is Cover of (T | A) & GE is countable ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in GE or x in FA ) assume A19: x in GE ; ::_thesis: x in FA then A20: x <> {} by ZFMISC_1:56; x in G | A by A19, ZFMISC_1:56; then consider R being Subset of T such that A21: R in G and A22: R /\ A = x by TOPS_2:def_3; percases ( R in RNG or R in AA ) by A16, A21, XBOOLE_0:def_3; suppose R in RNG ; ::_thesis: x in FA then consider y being set such that A23: y in dom f and A24: f . y = R by FUNCT_1:def_3; y = R /\ A by A6, A23, A24; hence x in FA by A22, A23; ::_thesis: verum end; suppose R in AA ; ::_thesis: x in FA then R = A ` by TARSKI:def_1; then x = A \ A by A22, SUBSET_1:13; hence x in FA by A20, XBOOLE_1:37; ::_thesis: verum end; end; end; union G = [#] T by A17, SETFAM_1:45; then [#] (T | A) = union (G | A) by A7, TOPS_2:33 .= union GE by PARTIT1:2 ; hence GE is Cover of (T | A) by SETFAM_1:def_11; ::_thesis: GE is countable A25: card (G | A) c= card G by Th7; card G c= omega by A18, CARD_3:def_14; then card (G | A) c= omega by A25, XBOOLE_1:1; then G | A is countable by CARD_3:def_14; hence GE is countable by CARD_3:95; ::_thesis: verum end; 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) proof let M be non empty MetrSpace; ::_thesis: 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) set TM = TopSpaceMetr M; let A, B be non empty Subset of (TopSpaceMetr M); ::_thesis: { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } is open Subset of (TopSpaceMetr M) set dA = dist_min A; set dB = dist_min B; consider g being Function of the carrier of (TopSpaceMetr M), the carrier of R^1 such that A1: for p being Point of (TopSpaceMetr M) for r1, r2 being real number st (dist_min A) . p = r1 & (dist_min B) . p = r2 holds g . p = r1 - r2 and A2: g is continuous by JGRAPH_2:21; set gA = { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ; reconsider A = ].-infty,0.[ as Subset of R^1 by TOPMETR:17; A3: A is open by BORSUK_5:40; A4: g " A c= { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g " A or x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ) assume A5: x in g " A ; ::_thesis: x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } then reconsider p = x as Point of (TopSpaceMetr M) ; A6: g . x in A by A5, FUNCT_1:def_7; ((dist_min A) . p) - ((dist_min B) . p) = g . x by A1; then ((dist_min A) . p) - ((dist_min B) . p) < 0 by A6, XXREAL_1:233; hence x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ; ::_thesis: verum end; A7: { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } c= g " A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } or x in g " A ) assume x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ; ::_thesis: x in g " A then consider p being Point of (TopSpaceMetr M) such that A8: p = x and A9: ((dist_min A) . p) - ((dist_min B) . p) < 0 ; g . p = ((dist_min A) . p) - ((dist_min B) . p) by A1; then ( dom g = [#] (TopSpaceMetr M) & g . p in A ) by A9, FUNCT_2:def_1, XXREAL_1:233; hence x in g " A by A8, FUNCT_1:def_7; ::_thesis: verum end; ( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} ) ; then g " A is open by A2, A3, TOPS_2:43; hence { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } is open Subset of (TopSpaceMetr M) by A4, A7, XBOOLE_0:def_10; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: 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 ) let A, B be Subset of TM; ::_thesis: ( A,B are_separated implies ex U, W being open Subset of TM st ( A c= U & B c= W & U misses W ) ) assume A1: A,B are_separated ; ::_thesis: ex U, W being open Subset of TM st ( A c= U & B c= W & U misses W ) set TOP = the topology of TM; set cTM = the carrier of TM; consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that A2: metr is_metric_of the carrier of TM and A3: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def_8; percases ( A = {} TM or B = {} TM or ( A <> {} TM & B <> {} TM ) ) ; supposeA4: A = {} TM ; ::_thesis: ex U, W being open Subset of TM st ( A c= U & B c= W & U misses W ) take {} TM ; ::_thesis: ex W being open Subset of TM st ( A c= {} TM & B c= W & {} TM misses W ) take [#] TM ; ::_thesis: ( A c= {} TM & B c= [#] TM & {} TM misses [#] TM ) thus ( A c= {} TM & B c= [#] TM & {} TM misses [#] TM ) by A4, XBOOLE_1:65; ::_thesis: verum end; supposeA5: B = {} TM ; ::_thesis: ex U, W being open Subset of TM st ( A c= U & B c= W & U misses W ) take [#] TM ; ::_thesis: ex W being open Subset of TM st ( A c= [#] TM & B c= W & [#] TM misses W ) take {} TM ; ::_thesis: ( A c= [#] TM & B c= {} TM & [#] TM misses {} TM ) thus ( A c= [#] TM & B c= {} TM & [#] TM misses {} TM ) by A5, XBOOLE_1:65; ::_thesis: verum end; supposeA6: ( A <> {} TM & B <> {} TM ) ; ::_thesis: ex U, W being open Subset of TM st ( A c= U & B c= W & U misses W ) then A7: not TM is empty ; then reconsider Tm = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A2, PCOMPS_1:36; set TTm = TopSpaceMetr Tm; reconsider A9 = A, B9 = B as Subset of (TopSpaceMetr Tm) by A2, A7, PCOMPS_2:4; set dA = dist_min A9; set dB = dist_min B9; reconsider U = { p where p is Point of Tm : ((dist_min A9) . p) - ((dist_min B9) . p) < 0 } , W = { p where p is Point of Tm : ((dist_min B9) . p) - ((dist_min A9) . p) < 0 } as open Subset of (TopSpaceMetr Tm) by A6, Lm12; ( U in Family_open_set Tm & W in Family_open_set Tm ) by PRE_TOPC:def_2; then reconsider U = U, W = W as open Subset of TM by A3, PRE_TOPC:def_2; take U ; ::_thesis: ex W being open Subset of TM st ( A c= U & B c= W & U misses W ) take W ; ::_thesis: ( A c= U & B c= W & U misses W ) A8: [#] TM = [#] (TopSpaceMetr Tm) by A2, A7, PCOMPS_2:4; thus A c= U ::_thesis: ( B c= W & U misses W ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in U ) assume A9: x in A ; ::_thesis: x in U then reconsider p = x as Point of Tm by A2, A7, PCOMPS_2:4; A misses Cl B by A1, CONNSP_1:def_1; then not x in Cl B by A9, XBOOLE_0:3; then not x in Cl B9 by A3, A8, TOPS_3:80; then A10: (dist_min B9) . p <> 0 by A6, HAUSDORF:8; A11: (dist_min B9) . p >= 0 by A6, JORDAN1K:9; (dist_min A9) . p = 0 by A9, HAUSDORF:5; then ((dist_min A9) . p) - ((dist_min B9) . p) < 0 by A10, A11; hence x in U ; ::_thesis: verum end; thus B c= W ::_thesis: U misses W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in W ) assume A12: x in B ; ::_thesis: x in W then reconsider p = x as Point of Tm by A2, A7, PCOMPS_2:4; B misses Cl A by A1, CONNSP_1:def_1; then not x in Cl A by A12, XBOOLE_0:3; then not x in Cl A9 by A3, A8, TOPS_3:80; then A13: (dist_min A9) . p <> 0 by A6, HAUSDORF:8; A14: (dist_min A9) . p >= 0 by A6, JORDAN1K:9; (dist_min B9) . p = 0 by A12, HAUSDORF:5; then ((dist_min B9) . p) - ((dist_min A9) . p) < 0 by A13, A14; hence x in W ; ::_thesis: verum end; thus U misses W ::_thesis: verum proof assume U meets W ; ::_thesis: contradiction then consider x being set such that A15: x in U and A16: x in W by XBOOLE_0:3; consider p being Point of Tm such that A17: p = x and A18: ((dist_min B9) . p) - ((dist_min A9) . p) < 0 by A16; ex q being Point of Tm st ( q = x & ((dist_min A9) . q) - ((dist_min B9) . q) < 0 ) by A15; then - (((dist_min A9) . p) - ((dist_min B9) . p)) > - 0 by A17; hence contradiction by A18; ::_thesis: verum end; end; end; 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 let TM be metrizable TopSpace; ::_thesis: for Am, Bm being Subset of TM st Am,Bm are_separated holds ex L being Subset of TM st L separates Am,Bm let Am, Bm be Subset of TM; ::_thesis: ( Am,Bm are_separated implies ex L being Subset of TM st L separates Am,Bm ) assume Am,Bm are_separated ; ::_thesis: ex L being Subset of TM st L separates Am,Bm then consider U, W being open Subset of TM such that A1: ( Am c= U & Bm c= W & U misses W ) by Lm13; take (U \/ W) ` ; ::_thesis: (U \/ W) ` separates Am,Bm thus (U \/ W) ` separates Am,Bm by A1, Def3; ::_thesis: verum 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 let TM be metrizable TopSpace; ::_thesis: 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 ) let M be Subset of TM; ::_thesis: 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 ) let A1, A2 be closed Subset of TM; ::_thesis: 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 ) let V1, V2 be open Subset of TM; ::_thesis: ( A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 implies 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 ) ) assume that A1: A1 c= V1 and A2: A2 c= V2 and A3: Cl V1 misses Cl V2 ; ::_thesis: 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 ) set TMM = TM | M; let mV1, mV2, mL be Subset of (TM | M); ::_thesis: ( mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 implies ex L being Subset of TM st ( L separates A1,A2 & M /\ L c= mL ) ) assume that A4: mV1 = M /\ (Cl V1) and A5: mV2 = M /\ (Cl V2) and A6: mL separates mV1,mV2 ; ::_thesis: ex L being Subset of TM st ( L separates A1,A2 & M /\ L c= mL ) A7: V2 /\ M c= mV2 by A5, PRE_TOPC:18, XBOOLE_1:26; consider U9, W9 being open Subset of (TM | M) such that A8: mV1 c= U9 and A9: mV2 c= W9 and A10: U9 misses W9 and A11: mL = (U9 \/ W9) ` by A6, Def3; A12: [#] (TM | M) = M by PRE_TOPC:def_5; then reconsider u = U9, w = W9 as Subset of TM by XBOOLE_1:1; set u1 = u \/ A1; set w1 = w \/ A2; A13: mV2 /\ u c= U9 /\ W9 by A9, XBOOLE_1:26; U9,W9 are_separated by A10, TSEP_1:37; then A14: u,w are_separated by CONNSP_1:5; V2 /\ u = V2 /\ (M /\ u) by A12, XBOOLE_1:28 .= (V2 /\ M) /\ u by XBOOLE_1:16 ; then V2 /\ u c= mV2 /\ u by A7, XBOOLE_1:26; then V2 /\ u c= U9 /\ W9 by A13, XBOOLE_1:1; then V2 /\ u c= {} by A10, XBOOLE_0:def_7; then V2 /\ u = {} ; then V2 misses u by XBOOLE_0:def_7; then A15: V2 misses Cl u by TSEP_1:36; A16: Cl (u \/ A1) misses w \/ A2 proof assume Cl (u \/ A1) meets w \/ A2 ; ::_thesis: contradiction then consider x being set such that A17: ( x in Cl (u \/ A1) & x in w \/ A2 ) by XBOOLE_0:3; A18: Cl (u \/ A1) = (Cl u) \/ (Cl A1) by PRE_TOPC:20; percases ( ( x in Cl u & x in w ) or ( x in Cl u & x in A2 ) or ( x in Cl A1 & x in w ) or ( x in Cl A1 & x in A2 ) ) by A17, A18, XBOOLE_0:def_3; suppose ( x in Cl u & x in w ) ; ::_thesis: contradiction then w meets Cl u by XBOOLE_0:3; hence contradiction by A14, CONNSP_1:def_1; ::_thesis: verum end; suppose ( x in Cl u & x in A2 ) ; ::_thesis: contradiction hence contradiction by A2, A15, XBOOLE_0:3; ::_thesis: verum end; supposeA19: ( x in Cl A1 & x in w ) ; ::_thesis: contradiction Cl A1 c= Cl V1 by A1, PRE_TOPC:19; then x in mV1 by A4, A12, A19, XBOOLE_0:def_4; hence contradiction by A8, A10, A19, XBOOLE_0:3; ::_thesis: verum end; supposeA20: ( x in Cl A1 & x in A2 ) ; ::_thesis: contradiction A21: ( Cl A1 c= Cl V1 & V2 c= Cl V2 ) by A1, PRE_TOPC:18, PRE_TOPC:19; x in V2 by A2, A20; hence contradiction by A3, A20, A21, XBOOLE_0:3; ::_thesis: verum end; end; end; A22: V1 /\ M c= mV1 by A4, PRE_TOPC:18, XBOOLE_1:26; A23: mV1 /\ w c= U9 /\ W9 by A8, XBOOLE_1:26; V1 /\ w = V1 /\ (M /\ w) by A12, XBOOLE_1:28 .= (V1 /\ M) /\ w by XBOOLE_1:16 ; then V1 /\ w c= mV1 /\ w by A22, XBOOLE_1:26; then V1 /\ w c= U9 /\ W9 by A23, XBOOLE_1:1; then V1 /\ w c= {} by A10, XBOOLE_0:def_7; then V1 /\ w = {} ; then V1 misses w by XBOOLE_0:def_7; then A24: V1 misses Cl w by TSEP_1:36; Cl (w \/ A2) misses u \/ A1 proof assume Cl (w \/ A2) meets u \/ A1 ; ::_thesis: contradiction then consider x being set such that A25: ( x in Cl (w \/ A2) & x in u \/ A1 ) by XBOOLE_0:3; A26: Cl (w \/ A2) = (Cl w) \/ (Cl A2) by PRE_TOPC:20; percases ( ( x in Cl w & x in u ) or ( x in Cl w & x in A1 ) or ( x in Cl A2 & x in u ) or ( x in Cl A2 & x in A1 ) ) by A25, A26, XBOOLE_0:def_3; suppose ( x in Cl w & x in u ) ; ::_thesis: contradiction then Cl w meets u by XBOOLE_0:3; hence contradiction by A14, CONNSP_1:def_1; ::_thesis: verum end; suppose ( x in Cl w & x in A1 ) ; ::_thesis: contradiction hence contradiction by A1, A24, XBOOLE_0:3; ::_thesis: verum end; supposeA27: ( x in Cl A2 & x in u ) ; ::_thesis: contradiction Cl A2 c= Cl V2 by A2, PRE_TOPC:19; then x in mV2 by A5, A12, A27, XBOOLE_0:def_4; hence contradiction by A9, A10, A27, XBOOLE_0:3; ::_thesis: verum end; supposeA28: ( x in Cl A2 & x in A1 ) ; ::_thesis: contradiction A29: ( Cl A2 c= Cl V2 & V1 c= Cl V1 ) by A2, PRE_TOPC:18, PRE_TOPC:19; x in V1 by A1, A28; hence contradiction by A3, A28, A29, XBOOLE_0:3; ::_thesis: verum end; end; end; then u \/ A1,w \/ A2 are_separated by A16, CONNSP_1:def_1; then consider U1, W1 being open Subset of TM such that A30: u \/ A1 c= U1 and A31: w \/ A2 c= W1 and A32: U1 misses W1 by Lm13; take L = (U1 \/ W1) ` ; ::_thesis: ( L separates A1,A2 & M /\ L c= mL ) A2 c= w \/ A2 by XBOOLE_1:7; then A33: A2 c= W1 by A31, XBOOLE_1:1; w c= w \/ A2 by XBOOLE_1:7; then A34: w c= W1 by A31, XBOOLE_1:1; u c= u \/ A1 by XBOOLE_1:7; then u c= U1 by A30, XBOOLE_1:1; then A35: u \/ w c= U1 \/ W1 by A34, XBOOLE_1:13; A1 c= u \/ A1 by XBOOLE_1:7; then A1 c= U1 by A30, XBOOLE_1:1; hence L separates A1,A2 by A32, A33, Def3; ::_thesis: M /\ L c= mL A36: ([#] (TM | M)) \ (U9 \/ W9) = mL by A11; M /\ L = (M /\ ([#] TM)) \ (U1 \/ W1) by XBOOLE_1:49 .= M \ (U1 \/ W1) by XBOOLE_1:28 ; then M /\ L c= M \ (U9 \/ W9) by A35, XBOOLE_1:34; hence M /\ L c= mL by A36, PRE_TOPC:def_5; ::_thesis: verum end;