:: Basic Properties of Metrizable Topological Spaces :: by Karol P\c{a}k :: :: Received March 31, 2009 :: Copyright (c) 2009 Association of Mizar Users environ vocabularies ABSVALUE, ARYTM, ARYTM_1, ARYTM_3, BOOLE, CARD_1, CARD_2, CARD_4, CARD_5, COMPTS_1, CONNSP_1, EUCLID, FINSET_1, FINSEQ_1, FINSEQ_2, FUNCOP_1, FUNCT_1, FUNCT_3, GROUP_1, GROUP_3, MCART_1, METRIC_1, NAGATA_1, NATTRA_1, ORDINAL2, PCOMPS_1, PRE_TOPC, PROB_1, RAT_1, RCOMP_1, RELAT_1, RLVECT_3, SETFAM_1, SUBSET_1, SUPINF_1, T_0TOPSP, TARSKI, TOPGEN_1, TOPGEN_4, TOPMETR, TOPREAL7, TOPS_1, TOPS_2, WAYBEL23, WEIERSTR, METRIZTS; notations BINOP_1, TOPMETR, CARD_1, CANTOR_1, COMPLEX1, FINSET_1, TARSKI, XBOOLE_0, RELAT_1, SUBSET_1, ORDINAL1, NUMBERS, ZFMISC_1, XREAL_0, REAL_1, DOMAIN_1, METRIC_1, PCOMPS_1, CARD_3, KURATO_2, WAYBEL23, TOPGEN_1, FUNCOP_1, XCMPLX_0, TOPS_1, CARD_2, NEWTON, BORSUK_1, NAGATA_1, TEX_2, TOPGEN_4, RCOMP_1, WEIERSTR, TOPREAL7, ORDERS_4, XXREAL_0, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_3, NAT_1, FINSEQ_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1, TOPS_2, BORSUK_3, EUCLID, FINSEQ_2; constructors REAL_1, KURATO_2, CANTOR_1, URYSOHN3, TOPGEN_4, WAYBEL23, TOPGEN_1, TOPS_1, FUNCT_3, TOPREAL9, CARD_2, NEWTON, CARD_5, NAGATA_1, TEX_2, TSP_1, CONNSP_1, RCOMP_1, WEIERSTR, TOPREAL7, ORDERS_4, TOPS_2, BORSUK_3, FUNCSDOM; registrations TOPMETR, PRE_TOPC, PCOMPS_1, XREAL_0, SUBSET_1, STRUCT_0, TOPS_1, METRIC_1, XXREAL_0, YELLOW13, CARD_1, XBOOLE_0, FINSET_1, FUNCT_1, ORDINAL1, COMPTS_1, RELAT_1, XCMPLX_0, CARD_LAR, BORSUK_1, TOPGEN_4, MEMBERED, TOPREAL7, BORSUK_3, EUCLID; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; definitions BINOP_1, CARD_3, METRIC_1, PCOMPS_1, PRE_TOPC, SUBSET_1, STRUCT_0, TARSKI, TOPS_2, XBOOLE_0; theorems ABSVALUE, BORSUK_1, BORSUK_5, CANTOR_1, CARD_1, CARD_2, CARD_3, CARD_4, COMPL_SP, CONNSP_1, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_3, HAUSDORF, JGRAPH_2, JORDAN1K, MCART_1, METRIC_1, NAGATA_1, NAGATA_2, NEWTON, PARTIT1, PCOMPS_1, PCOMPS_2, PREPOWER, PRE_TOPC, PROB_1, SETFAM_1, SUBSET_1, TARSKI, TEX_2, TMAP_1, TOPGEN_1, TOPGEN_2, TOPGEN_4, TOPMETR, TOPREAL7, TOPS_1, TOPS_2, TSEP_1, TSP_1, WAYBEL23, WAYBEL29, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0, XXREAL_1, YELLOW12, YELLOW_9, ZFMISC_1, T_0TOPSP, TOPGRP_1, RELAT_1, ORDERS_4, NUMBERS, TOPREAL6, TOPREALA, EUCLID, ORDINAL1, FINSEQ_2, YELLOW14, TOPS_3; schemes BORSUK_2, CLASSES1, FRAENKEL, FUNCT_2, LMOD_7, NAT_1; begin :: Preliminaries reserve T, T1, T2 for TopSpace, A, B for Subset of T, F, G for Subset-Family of T, A1 for Subset of T1, A2 for Subset of T2, TM, TM1, TM2 for metrizable TopSpace, Am, Bm for Subset of TM, Fm, Gm for Subset-Family of TM, C for Cardinal, iC for infinite Cardinal; definition let T1,T2,A1,A2; pred A1,A2 are_homeomorphic means :Def1: T1|A1,T2|A2 are_homeomorphic; end; Lm1: for T1,T2 be empty TopSpace holds T1,T2 are_homeomorphic proof let T1,T2 be empty TopSpace; reconsider E={} as Function of T1,T2 by FUNCT_2:3,RELAT_1:60; A1: [#]T2={} iff [#]T1={}; for P be Subset of T2 st P is open holds E"P is open; then A2: E is continuous by A1,TOPS_2:55; for P be Subset of T1 st P is open holds(E")"P is open; then E" is continuous by A1,TOPS_2:55; then E is being_homeomorphism by A1,A2,RELAT_1:60,TOPS_2:def 5; hence thesis by T_0TOPSP:def 1; end; theorem T1,T2 are_homeomorphic iff [#]T1,[#]T2 are_homeomorphic proof A1: T1|([#]T1)=the TopStruct of T1 & T2|([#]T2)=the TopStruct of T2 by TSEP_1:100; per cases; suppose A3: T2 is non empty; hereby assume T1,T2 are_homeomorphic; then the TopStruct of T1,the TopStruct of T2 are_homeomorphic by A3,TOPREALA:36; hence [#]T1,[#]T2 are_homeomorphic by A1,Def1; end; assume[#]T1,[#]T2 are_homeomorphic; then the TopStruct of T1,the TopStruct of T2 are_homeomorphic by A1,Def1; hence thesis by A3,TOPREALA:36; end; suppose A4: T2 is empty; hereby assume T1,T2 are_homeomorphic; then T1 is empty iff T2 is empty by YELLOW14:19; then T1|([#]T1),T2|([#]T2) are_homeomorphic by A4,Lm1; hence [#]T1,[#]T2 are_homeomorphic by Def1; end; assume [#]T1,[#]T2 are_homeomorphic; then T1|([#]T1),T2|([#]T2) are_homeomorphic by Def1; then T1 is empty by A4,YELLOW14:19; hence thesis by A4,Lm1; end; end; theorem Th2: for f be Function of T1,T2 st f is being_homeomorphism for g be Function of T1|A1,T2|(f.:A1) st g = f|A1 holds g is being_homeomorphism proof let f be Function of T1,T2 such that A1: f is being_homeomorphism; AA: T1,T2 are_homeomorphic by A1,T_0TOPSP:def 1; set B= f.:A1; A2: dom f=[#]T1 by A1,TOPS_2:def 5; A3: rng f=[#]T2 by A1,TOPS_2:def 5; T1 is empty iff T2 is empty by YELLOW14:19,AA; then A4: [#]T1={} iff [#]T2={}; let g be Function of T1|A1,T2|B such that A5: g=f|A1; A6: rng g=B by A5,RELAT_1:148; set TA=T1|A1,TB=T2|B; K: [#]TA = A1 & [#]TB = B by PRE_TOPC:def 10; A7: dom g = dom f/\A1 by A5,RELAT_1:90 .= A1 by A2,XBOOLE_1:28; then TA is empty iff TB is empty by K,A6,YELLOW14:19; then A8: [#]TA={} iff [#]TB={}; A9: [#]TA=A1 by PRE_TOPC:def 10; A10: f is one-to-one by A1,TOPS_2:def 5; then A11: g is one-to-one by A5,FUNCT_1:84; A12: [#]TB=B by PRE_TOPC:def 10; A13: f is continuous by A1,TOPS_2:def 5; for P be Subset of TB st P is open holds g"P is open proof let P be Subset of TB; assume P is open; then consider P1 be Subset of T2 such that A14: P1 is open and A15: P=P1/\B by A12,TSP_1:def 1; reconsider PA=f"P1/\A1 as Subset of TA by A9,XBOOLE_1:17; A16: A1/\PA=PA by XBOOLE_1:17,28; A1=f"B by A2,A10,FUNCT_1:164; then PA=f"P by A15,FUNCT_1:137; then A17: g"P=PA by A5,A16,FUNCT_1:139; f"P1 is open by A13,A4,A14,TOPS_2:55; hence thesis by A9,A17,TSP_1:def 1; end; then A18: g is continuous by A8,TOPS_2:55; A19: f" is continuous by A1,TOPS_2:def 5; for P be Subset of TA st P is open holds(g")"P is open proof let P be Subset of TA; assume P is open; then consider P1 be Subset of T1 such that A20: P1 is open and A21: P=P1/\A1 by A9,TSP_1:def 1; reconsider PB=(f")"P1/\B as Subset of TB by A12,XBOOLE_1:17; A22: (f")"P1 is open by A19,A4,A20,TOPS_2:55; B = (f")"A1 by A3,A10,TOPS_2:67; then PB = (f")"(P1/\A1) by FUNCT_1:137 .= f.:P by A3,A10,A21,TOPS_2:67 .= g.:P by A5,A9,RELAT_1:162 .= (g")"P by A12,A6,A11,TOPS_2:67; hence thesis by A12,A22,TSP_1:def 1; end; then g" is continuous by A8,TOPS_2:55; hence thesis by A9,A12,A7,A6,A11,A18,TOPS_2:def 5; end; theorem for f be Function of T1,T2 st f is being_homeomorphism holds A1,f.:A1 are_homeomorphic proof let f be Function of T1,T2 such that A1: f is being_homeomorphism; dom f=[#]T1 by A1,TOPS_2:def 5; then A2: dom(f|A1) = [#]T1/\A1 by RELAT_1:90 .= A1 by XBOOLE_1:28 .= [#](T1|A1) by PRE_TOPC:def 10; rng(f|A1) = f.:A1 by RELAT_1:148 .= [#](T2|(f.:A1)) by PRE_TOPC:def 10; then reconsider g=f|A1 as Function of T1|A1,T2|(f.:A1) by A2,FUNCT_2:3; g is being_homeomorphism by A1,Th2; then T1|A1,T2|(f.:A1)are_homeomorphic by T_0TOPSP:def 1; hence thesis by Def1; end; Lm2: for T1,T2 be non empty TopSpace st T1,T2 are_homeomorphic holds weight T2 c=weight T1 proof defpred P[set] means not contradiction; let T1,T2 be non empty TopSpace; consider B1 be Basis of T1 such that A1: card B1=weight T1 by WAYBEL23:75; defpred PP[set] means $1 in B1 & P[$1]; assume T1,T2 are_homeomorphic; then consider f be Function of T1,T2 such that A2: f is being_homeomorphism by T_0TOPSP:def 1; deffunc F(Subset of T1)=f.:$1; consider B2 be Subset-Family of T2 such that A3: B2={F(w) where w is Subset of T1:PP[w]} from LMOD_7:sch 5; A4: for A be Subset of T2 st A is open for p be Point of T2 st p in A ex a be Subset of T2 st a in B2 & p in a & a c=A proof let A be Subset of T2 such that A5: A is open; A6: f"A is open by A2,A5,TOPGRP_1:26; let p be Point of T2 such that A7: p in A; A8: rng f=[#]T2 by A2,TOPGRP_1:25; then consider x be set such that A9: x in dom f and A10: f.x=p by FUNCT_1:def 5; A11: x in f"A by A7,A9,A10,FUNCT_1:def 13; reconsider x as Point of T1 by A9; consider a1 be Subset of T1 such that A12: a1 in B1 & x in a1 and A13: a1 c=f"A by A11,A6,YELLOW_9:31; take a=F(a1); a c=f.:(f"A) by A13,RELAT_1:156; hence thesis by A3,A8,A9,A10,A12,FUNCT_1:147,def 12; end; A14: B1 c=the topology of T1 by CANTOR_1:def 2; B2 c=the topology of T2 proof let x be set; assume x in B2; then consider w be Subset of T1 such that A15: x=F(w) and A16: PP[w] by A3; w is open by A14,A16,PRE_TOPC:def 5; then F(w) is open by A2,TOPGRP_1:25; hence thesis by A15,PRE_TOPC:def 5; end; then reconsider B2 as Basis of T2 by A4,YELLOW_9:32; A17: card{F(w) where w is Subset of T1:PP[w]}c=card B1 from BORSUK_2:sch 1; weight T2 c=card B2 by WAYBEL23:74; hence thesis by A1,A3,A17,XBOOLE_1:1; end; Lm3: for T be empty TopSpace holds weight T is empty proof let T be empty TopSpace; reconsider B={} as empty Subset-Family of T by TOPGEN_4:18; A1: B c=the topology of T by XBOOLE_1:2; for A be Subset of T st A is open for p be Point of T st p in A ex a be Subset of T st a in B & p in a & a c=A; then reconsider B as Basis of T by A1,YELLOW_9:32; weight T c=card B by WAYBEL23:74; hence thesis; end; theorem Th4: T1,T2 are_homeomorphic implies weight T1 = weight T2 proof assume A1: T1,T2 are_homeomorphic; per cases; suppose A3: [#]T1={} or [#]T2={}; A: T1 is empty iff T2 is empty by A1,YELLOW14:19; then weight T1=0 by Lm3,A3; hence thesis by Lm3,A,A3; end; suppose T1 is non empty & T2 is non empty; then weight T2 c=weight T1 & weight T1 c=weight T2 by A1,Lm2; hence thesis by XBOOLE_0:def 10; end; end; registration cluster empty -> metrizable TopSpace; coherence proof let T be TopSpace; set cT=the carrier of T; A1: dom{}={} & rng{}c=REAL by XBOOLE_1:2; assume A2: T is empty; then A3: bool cT={{}} by ZFMISC_1:1; cT = {} by A2; then [:cT,cT:]={} by ZFMISC_1:113; then reconsider E={} as Function of[:cT,cT:],REAL by A1,FUNCT_2:4; take E; set M=SpaceMetr(cT,E); for a,b,c be Element of cT holds (E.(a,b)=0 iff a=b) & E.(a,b)=E.(b,a) & E.(a,c)<=E.(a,b)+E.(b,c) proof let a,b,c be Element of cT; not[{},{}] in dom E; then A4: E.({},{})={} by FUNCT_1:def 4; a={} & b={} by A2,SUBSET_1:def 2; hence thesis by A4; end; hence E is_metric_of cT by PCOMPS_1:def 7; then A5: M=MetrStruct(# cT,E #) by PCOMPS_1:def 8; then cT in Family_open_set(M) by PCOMPS_1:34; then Family_open_set(M)={{}} by A3,A5,ZFMISC_1:39; hence thesis by A3,ZFMISC_1:39; end; cluster metrizable -> T_4 TopSpace; coherence proof let T be TopSpace such that A6: T is metrizable; per cases; suppose A7: T is empty; for F1,F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 ex G1,G2 be Subset of T st G1 is open & G2 is open & F1 c=G1 & F2 c=G2 & G1 misses G2 by A7; then T is normal by PRE_TOPC:def 18; hence thesis by A7; end; suppose T is non empty; then reconsider t=T as metrizable(non empty TopSpace) by A6; A9: t is T_1 by NAGATA_2:19; t is regular & ex Bn being FamilySequence of t st Bn is Basis_sigma_locally_finite by NAGATA_2:19; then T is normal by A9,NAGATA_1:20; hence thesis by A9; end; end; let M be MetrSpace; cluster TopSpaceMetr M -> metrizable; coherence proof per cases; suppose M is empty; then TopSpaceMetr(M) is empty; hence thesis; end; suppose M is non empty; then reconsider m=M as non empty MetrSpace; set TM=TopSpaceMetr(M); reconsider CM=[#]M as non empty Subset of m; reconsider CTM=[#]TM as Subset of TM; set TMM=TopSpaceMetr(m|CM); A10: [#](m|CM)=CM by TOPMETR:def 2; then reconsider D=the distance of m|CM as Function of [:the carrier of TM,the carrier of TM:],REAL; take D; A11: D is_metric_of the carrier of TM by A10,PCOMPS_1:39; TM|CTM=TMM & TM is SubSpace of TM by HAUSDORF:18,TSEP_1:2; then the topology of TopSpaceMetr M = the topology of TopSpaceMetr(m|CM) by A10,TSEP_1:5 .= Family_open_set(SpaceMetr(the carrier of TM,D)) by A10,A11,PCOMPS_1:def 8; hence thesis by A10,PCOMPS_1:39; end; end; end; registration let TM,Am; cluster TM|Am -> metrizable; coherence proof per cases; suppose Am is empty; hence thesis; end; suppose A1: Am is non empty; consider metr be 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 9; set TMM=SpaceMetr(the carrier of TM,metr); A4: TM is non empty by A1; then reconsider TMM=SpaceMetr(the carrier of TM,metr) as non empty MetrSpace by A2,PCOMPS_1:40; reconsider Atm=Am as non empty Subset of TMM by A1,A2,A4,PCOMPS_2:8; 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:8,TSEP_1:2; then TopSpaceMetr TMM is SubSpace of TM by A3,TMAP_1:11; 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:18,PRE_TOPC:def 10; hence thesis by A5,PRE_TOPC:def 10; end; end; end; registration let TM1,TM2; cluster [:TM1,TM2:] -> metrizable; coherence proof per cases; suppose[:TM1,TM2:] is empty; hence thesis; end; suppose A1: [:TM1,TM2:] is non empty; then A2: TM1 is non empty; consider metr1 be Function of [:the carrier of TM1, the carrier of TM1:],REAL such that A3: metr1 is_metric_of the carrier of TM1 and A4: Family_open_set(SpaceMetr(the carrier of TM1,metr1)) = the topology of TM1 by PCOMPS_1:def 9; set tm1=SpaceMetr(the carrier of TM1,metr1); consider metr2 be Function of[:the carrier of TM2, the carrier of TM2:],REAL such that A5: metr2 is_metric_of the carrier of TM2 and A6: Family_open_set(SpaceMetr(the carrier of TM2,metr2)) = the topology of TM2 by PCOMPS_1:def 9; set tm2=SpaceMetr(the carrier of TM2,metr2); A7: TM2 is non empty by A1; then reconsider tm1,tm2 as non empty MetrStruct by A5,A3,A2,PCOMPS_1:40; A8: the TopStruct of TM1=the TopStruct of TopSpaceMetr(tm1) by A3,A4,A2,PCOMPS_2:8; the TopStruct of TM2=the TopStruct of TopSpaceMetr(tm2) by A7,A5,A6,PCOMPS_2:8; then [:TM1,TM2:] = [:TopSpaceMetr(tm1),TopSpaceMetr(tm2):] by A8,WAYBEL29:10 .= TopSpaceMetr max-Prod2(tm1,tm2) by TOPREAL7:25; hence thesis; end; end; end; registration let T be empty TopSpace; cluster weight T -> empty; coherence by Lm3; end; theorem Th5: weight [:T1,T2:] c= weight T1 *` weight T2 proof per cases; suppose T1 is empty or T2 is empty; hence thesis; end; suppose A1: T1 is non empty & T2 is non empty; consider B1 be Basis of T1 such that A2: card B1=weight T1 by WAYBEL23:75; consider B2 be Basis of T2 such that A3: card B2=weight T2 by WAYBEL23:75; 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,B2,B12 as non empty set by A1,YELLOW12:34; deffunc F(Element of[:B1,B2:])=[:$1`1,$1`2:]; A4: for x be Element of[:B1,B2:] holds F(x) is Element of B12 proof let x be Element of[:B1,B2:]; x`1 in B1 & x`2 in B2; then F(x) in B12; hence thesis; end; consider f be Function of[:B1,B2:],B12 such that A5: for x be Element of[:B1,B2:] holds f.x=F(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; assume x in B12; then consider a be Subset of T1,b be 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:106; [a,b]`1=a & [a,b]`2=b by MCART_1:7; then x=f.ab by A5,A7; hence thesis by A6,FUNCT_1:def 5; end; then A9: weight[:T1,T2:]c=card B12 & card B12 c=card[:B1,B2:] by A6,CARD_1:28,WAYBEL23:74; card[:B1,B2:]=card[:card B1,card B2:] by CARD_2:14 .=(card B1)*`card B2 by CARD_2:def 2; hence thesis by A3,A2,A9,XBOOLE_1:1; end; end; theorem Th6: T1 is non empty & T2 is non empty implies weight T1 c= weight [:T1,T2:] & weight T2 c= weight[:T1,T2:] proof defpred P[set] means not contradiction; set PR2=pr2(the carrier of T1,the carrier of T2); set PR1=pr1(the carrier of T1,the carrier of T2); assume T1 is non empty & T2 is non empty; then reconsider t1=T1,t2=T2 as non empty TopSpace; reconsider T12=[:t1,t2:] as non empty TopSpace; consider B12 be Basis of T12 such that A1: card B12=weight T12 by WAYBEL23:75; defpred PP[set] means $1 in B12 & P[$1]; deffunc F1(Subset of T12)=PR1.:$1; consider B1 be Subset-Family of T1 such that A2: B1={F1(w) where w is Subset of T12:PP[w]} from LMOD_7:sch 5; A3: B12 c=the topology of T12 by CANTOR_1:def 2; A4: B1 c=the topology of T1 proof let x be set; assume x in B1; then consider w be Subset of T12 such that A5: x=F1(w) and A6: PP[w] by A2; w is open by A3,A6,PRE_TOPC:def 5; then F1(w) is open by BORSUK_1:59; hence thesis by A5,PRE_TOPC:def 5; end; for A be Subset of T1 st A is open for p be Point of T1 st p in A ex a be Subset of T1 st a in B1 & p in a & a c=A proof let A be Subset of T1 such that A7: A is open; A8: [:A,[#]T2:] is open by A7,BORSUK_1:46; set p2=the Point of T2; A9: p2 in [#]t2; let p1 be Point of T1 such that A10: p1 in A; A11: [p1,p2] in [:A,[#]T2:] by A9,A10,ZFMISC_1:106; then reconsider p=[p1,p2] as Point of T12; consider a12 be Subset of T12 such that A12: a12 in B12 and A13: p in a12 and A14: a12 c=[:A,[#]T2:] by A8,A11,YELLOW_9:31; p1 in [#]t1 & p2 in [#]t2; then A15: PR1.(p1,p2)=p1 by FUNCT_3:def 5; a12 is open by A3,A12,PRE_TOPC:def 5; then reconsider a=F1(a12) as open Subset of T1 by BORSUK_1:59; take a; dom PR1 = [:[#]T1,[#]T2:] by FUNCT_3:def 5 .= [#]T12 by BORSUK_1:def 5; hence a in B1 & p1 in a by A2,A12,A13,A15,FUNCT_1:def 12; let y be set; assume y in a; then consider x be set such that A16: x in dom PR1 and A17: x in a12 & y=PR1.x by FUNCT_1:def 12; consider x1,x2 be set such that A18: x1 in [#]T1 & x2 in [#]T2 and A19: x=[x1,x2] by A16,ZFMISC_1:def 2; PR1.(x1,x2)=x1 by A18,FUNCT_3:def 5; hence thesis by A14,A17,A19,ZFMISC_1:106; end; then reconsider B1 as Basis of T1 by A4,YELLOW_9:32; A20: card{F1(w) where w is Subset of T12:PP[w]} c= card B12 from BORSUK_2:sch 1; weight t1 c=card B1 by WAYBEL23:74; hence weight T1 c=weight[:T1,T2:] by A1,A2,A20,XBOOLE_1:1; deffunc F2(Subset of T12)=PR2.:$1; consider B2 be Subset-Family of T2 such that A21: B2={F2(w) where w is Subset of T12:PP[w]} from LMOD_7:sch 5; A22: for A be Subset of T2 st A is open for p be Point of T2 st p in A ex a be Subset of T2 st a in B2 & p in a & a c=A proof let A be Subset of T2 such that A23: A is open; A24: [:[#]T1,A:] is open by A23,BORSUK_1:46; set p1=the Point of T1; A25: p1 in [#]t1; let p2 be Point of T2 such that A26: p2 in A; A27: [p1,p2] in [:[#]T1,A:] by A25,A26,ZFMISC_1:106; then reconsider p=[p1,p2] as Point of T12; consider a12 be Subset of T12 such that A28: a12 in B12 and A29: p in a12 and A30: a12 c=[:[#]T1,A:] by A24,A27,YELLOW_9:31; p1 in [#]t1 & p2 in [#]t2; then A31: PR2.(p1,p2)=p2 by FUNCT_3:def 6; a12 is open by A3,A28,PRE_TOPC:def 5; then reconsider a=F2(a12) as open Subset of T2 by BORSUK_1:59; take a; dom PR2 = [:[#]T1,[#]T2:] by FUNCT_3:def 6 .= [#]T12 by BORSUK_1:def 5; hence a in B2 & p2 in a by A21,A28,A29,A31,FUNCT_1:def 12; let y be set; assume y in a; then consider x be set such that A32: x in dom PR2 and A33: x in a12 & y=PR2.x by FUNCT_1:def 12; consider x1,x2 be set such that A34: x1 in [#]T1 & x2 in [#]T2 and A35: x=[x1,x2] by A32,ZFMISC_1:def 2; PR2.(x1,x2)=x2 by A34,FUNCT_3:def 6; hence thesis by A30,A33,A35,ZFMISC_1:106; end; B2 c=the topology of T2 proof let x be set; assume x in B2; then consider w be Subset of T12 such that A36: x=F2(w) and A37: PP[w] by A21; w is open by A3,A37,PRE_TOPC:def 5; then F2(w) is open by BORSUK_1:59; hence thesis by A36,PRE_TOPC:def 5; end; then reconsider B2 as Basis of T2 by A22,YELLOW_9:32; A38: card{F2(w) where w is Subset of T12:PP[w]}c=card B12 from BORSUK_2:sch 1; weight T2 c=card B2 by WAYBEL23:74; hence thesis by A1,A21,A38,XBOOLE_1:1; end; registration let T1,T2 be second-countable TopSpace; cluster [:T1,T2:] -> second-countable; coherence proof weight T1 c=omega & weight T2 c=omega by WAYBEL23:def 6; then A1: weight T1*`weight T2 c=omega by CARD_3:136,CARD_4:54; weight[:T1,T2:]c=weight T1 *` weight T2 by Th5; then weight[:T1,T2:]c=omega by A1,XBOOLE_1:1; hence thesis by WAYBEL23:def 6; end; end; theorem Th7: card (F|A) c= card F proof set FA=F|A; per cases; suppose FA is empty; hence thesis; end; suppose A1: FA is non empty; deffunc F(set)=$1/\A; A2: A=[#](T|A) by PRE_TOPC:def 10; A3: for x be set st x in F holds F(x) in FA proof let x be set; assume A4: x in F; F(x)c=A by XBOOLE_1:17; hence thesis by A2,A4,TOPS_2:def 3; end; consider g be Function of F,FA such that A5: for x be set st x in F holds g.x=F(x) from FUNCT_2:sch 2(A3); A6: dom g=F by A1,FUNCT_2:def 1; FA c=rng g proof let x be set; assume x in FA; then consider B such that A7: B in F and A8: F(B)=x by TOPS_2:def 3; x=g.B by A5,A7,A8; hence thesis by A6,A7,FUNCT_1:def 5; end; hence thesis by A6,CARD_1:28; end; end; theorem Th8: for Bas be Basis of T holds Bas|A is Basis of T|A proof let Bas be Basis of T; set BasA=Bas|A; set TA=T|A; A1: for U be Subset of TA st U is open for p be Point of TA st p in U ex a be Subset of TA st a in BasA & p in a & a c=U proof let U be Subset of TA such that A2: U is open; consider W be Subset of T such that A3: W is open and A4: U=W/\the carrier of TA by A2,TSP_1:def 1; let p be Point of TA such that A5: p in U; p in W by A4,A5,XBOOLE_0:def 4; then consider Wb be Subset of T such that A6: Wb in Bas and A7: p in Wb and A8: Wb c=W by A3,YELLOW_9:31; A9: Wb/\A in BasA by A6,TOPS_2:41; then reconsider WbA=Wb/\A as Subset of TA; A10: [#]TA=A by PRE_TOPC:def 10; then p in WbA by A5,A7,XBOOLE_0:def 4; hence thesis by A4,A8,A9,A10,XBOOLE_1:26; end; BasA c=the topology of TA proof let x be set such that A11: x in BasA; reconsider U=x as Subset of TA by A11; Bas c=the topology of T by CANTOR_1:def 2; then Bas is open by CANTOR_1:3,TOPS_2:18; then BasA is open by TOPS_2:47; then U is open by A11,TOPS_2:def 1; hence thesis by PRE_TOPC:def 5; end; hence thesis by A1,YELLOW_9:32; end; registration let T be second-countable TopSpace; let A be Subset of T; cluster T|A -> second-countable; coherence proof consider B be Basis of T such that A1: card B=weight T by WAYBEL23:75; B|A is Basis of T|A by Th8; then A2: weight(T|A)c=card(B|A) by WAYBEL23:74; 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 thesis by WAYBEL23:def 6; end; end; registration let M be non empty MetrSpace; let A be non empty Subset of TopSpaceMetr M; :: General Topology Th 4.1.10 cluster dist_min A -> continuous; coherence proof set TM=TopSpaceMetr M; set d=dist_min A; A1: for P being Subset of R^1 st P is open holds d"P is open proof let P be Subset of R^1; assume A2: P is open; for p be Point of M st p in d"P ex r be real number st r>0 & Ball(p,r)c=d"P proof reconsider P'=P as open Subset of TopSpaceMetr(RealSpace) by A2,TOPMETR:def 7; let p be Point of M; assume p in d"P; then A3: d.p in P by FUNCT_1:def 13; then reconsider dp=d.p as Point of RealSpace by TOPMETR:def 7; consider r be real number such that A4: r>0 and A5: Ball(dp,r)c=P' by A3,TOPMETR:22; take r; thus r>0 by A4; thus Ball(p,r)c=d"P proof let x be set; assume A6: x in Ball(p,r); then reconsider q=x as Point of M; A7: dist(p,q) F_sigma Subset of TM; coherence proof let Am; set TOP=the topology of TM,cTM=the carrier of TM; assume A1: Am is open; per cases; suppose A2: TM is empty; reconsider E={} as empty Subset-Family of TM by TOPGEN_4:18; Am=union E by A2,ZFMISC_1:2; hence thesis by TOPGEN_4:def 6; end; suppose A3: TM is non empty; per cases; suppose Am=[#]TM; hence thesis by A3; end; suppose A4: Am<>[#]TM; consider metr be Function of[:cTM,cTM:],REAL such that A5: metr is_metric_of cTM and A6: Family_open_set(SpaceMetr(cTM,metr))=TOP by PCOMPS_1:def 9; reconsider Tm=SpaceMetr(cTM,metr) as non empty MetrSpace by A3,A5,PCOMPS_1:40; set TTm=TopSpaceMetr Tm; Am in the topology of TTm by A1,A6,PRE_TOPC:def 5; then reconsider a=Am as open Subset of TTm by PRE_TOPC:def 5; ({}TTm)`=[#]TTm; then reconsider A'=a` as closed non empty Subset of TTm by A3,A4,A5, PCOMPS_2:8; defpred P[set,set] means for n be Nat st n=$1 holds$2={p where p is Point of TTm: (dist_min A').p<1/(2|^n)}; A7: for x be set st x in NAT ex y be set st y in TOP & P[x,y] proof let x be set; assume x in NAT; then reconsider n=x as Element of NAT; reconsider BallA={p where p is Point of TTm: (dist_min A').p<1/(2|^n)} as open Subset of TTm by Lm5; take BallA; thus thesis by A6,PRE_TOPC:def 5; end; consider p be Function of NAT,TOP such that A8: for x be set st x in NAT holds P[x,p.x] from FUNCT_2:sch 1(A7); TOP is open by CANTOR_1:3; then reconsider RNG=rng p as open Subset-Family of TM by TOPS_2:18,XBOOLE_1:1; set Crng=COMPLEMENT(RNG); A9: dom p=NAT by FUNCT_2:def 1; A10: [#]TM=[#]TTm by A3,A5,PCOMPS_2:8; A11: union Crng = Am proof hereby let x be set; assume A12: x in union Crng; then consider y be 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 8; then consider n be set such that A15: n in dom p and A16: p.n=Y` by FUNCT_1:def 5; reconsider n as Element of NAT by A15; assume not x in Am; then x in A' by A10,A12,XBOOLE_0:def 5; then A17: 2|^n>0 & (dist_min A').x=0 by HAUSDORF:5,PREPOWER:13; Y`={q where q is Point of TTm:(dist_min A').q<1/(2|^n)} by A8,A16; then x in Y` by A10,A12,A17; hence contradiction by A13,XBOOLE_0:def 5; end; let x be set; assume A18: x in Am; then reconsider q=x as Point of TTm by A3,A5,PCOMPS_2:8; Cl A'=A' & not q in A' by A18,PRE_TOPC:52,XBOOLE_0:def 5; then A19: (dist_min A').q<>0 by HAUSDORF:10; (dist_min A').q>=0 by JORDAN1K:9; then consider n be Element of NAT such that A20: 1/(2|^n)<=(dist_min A').q by A19,PREPOWER:106; p.n in RNG by A9,FUNCT_1:def 5; then reconsider pn=p.n as Subset of TM; A21: for s be Point of TTm st s=q holds not 1/(2|^n)>(dist_min A').s by A20; pn={s where s is Point of TTm:(dist_min A').s<1/(2|^n)} by A8; 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 5; then pn` in Crng by SETFAM_1:def 8; hence thesis by A22,TARSKI:def 4; end; Crng is closed & RNG is countable by A9,CARD_3:127,TOPS_2:17; hence thesis by A11,TOPGEN_4:def 6; end; end; end; cluster closed -> G_delta Subset of TM; coherence proof let Am; assume A23: Am is closed; per cases; suppose A24: TM is empty; reconsider E={} as empty Subset-Family of TM by TOPGEN_4:18; Am=meet E by A24,SETFAM_1:2; hence thesis by TOPGEN_4:def 7; end; suppose TM is non empty; then Am`` is G_delta by A23,TOPGEN_4:39; hence thesis; end; end; end; theorem for F be Subset of T|B st A is F_sigma & F = A/\B holds F is F_sigma proof let F be Subset of T|B; assume that A1: A is F_sigma and A2: F=A/\B; consider G be closed countable 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; assume x in union(G|B); then consider g be set such that A5: x in g and A6: g in G|B by TARSKI:def 4; consider h be 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 thesis by A2,A9,XBOOLE_0:def 4; end; card(G|B)c=card G & card G c=omega by Th7,CARD_3:def 15; then card(G|B)c=omega by XBOOLE_1:1; then A10: G|B is closed & G|B is countable by CARD_3:def 15,TOPS_2:48; A/\B/\B = A/\(B/\B) by XBOOLE_1:16 .= F by A2; then F c=union(G|B) by A3,TOPS_2:42,XBOOLE_1:17; then F=union(G|B) by A4,XBOOLE_0:def 10; hence thesis by A10,TOPGEN_4:def 6; end; theorem for F be Subset of T|B st A is G_delta & F = A/\B holds F is G_delta proof let F be Subset of T|B; assume that A1: A is G_delta and A2: F = A/\B; consider G be open countable 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; assume A5: x in meet(G|B); then consider g be set such that A6: g in G|B by SETFAM_1:2,XBOOLE_0:def 1; reconsider g as Subset of T|B by A6; A7: ex h be 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 let Y be set; assume Y in G; then Y/\B in G|B by TOPS_2:41; then x in Y/\B by A5,SETFAM_1:def 1; hence x in Y by XBOOLE_0:def 4; end; then x in A by A3,A7,SETFAM_1:def 1; hence thesis by A2,A8,XBOOLE_0:def 4; end; card(G|B)c=card G & card G c=omega by Th7,CARD_3:def 15; then card(G|B)c=omega by XBOOLE_1:1; then A9: G|B is open & G|B is countable by CARD_3:def 15,TOPS_2:47; F c=meet(G|B) proof let x be set; assume A10: x in F; then A11: x in A by A2,XBOOLE_0:def 4; A12: x in B by A2,A10,XBOOLE_0:def 4; A13: now let f be set; assume f in G|B; then consider h be 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; end; ex y be set st y in G by A3,A11,SETFAM_1:2,XBOOLE_0:def 1; then G|B is non empty by TOPS_2:41; hence thesis by A13,SETFAM_1:def 1; end; then F=meet(G|B) by A4,XBOOLE_0:def 10; hence thesis by A9,TOPGEN_4:def 7; end; theorem Th13: T is T_1 & A is discrete implies A is open Subset of T|(Cl A) proof assume that A1: T is T_1 and A2: A is discrete; set TA=T|(Cl A); A3: [#]TA=Cl A by PRE_TOPC:def 10; A4: A c=Cl A by PRE_TOPC:48; per cases; suppose TA is empty; hence thesis by A3,PRE_TOPC:48; end; suppose TA is non empty; then reconsider TA as non empty TopSpace; deffunc F(Element of TA)={$1}; defpred P[set] means $1 in A; consider S be Subset-Family of TA such that A5: S={F(x) where x is Element of TA:P[x]} from LMOD_7:sch 5; A6: S is open proof let B be Subset of TA; assume B in S; then consider y be Element of TA such that A7: B=F(y) and A8: P[y] by A5; reconsider x=y as Point of T by A8; consider G be Subset of T such that A9: G is open and A10: A/\G={x} by A2,A8,TEX_2:32; reconsider X={x} as Subset of T by A10; T is non empty by A7; then A11: Cl X=X by A1,PRE_TOPC:52; 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:40; then G/\Cl A=X by A11,A12,ZFMISC_1:39; hence thesis by A3,A7,A9,TSP_1:def 1; end; union S=A proof hereby let x be set; assume x in union S; then consider y be set such that A13: x in y and A14: y in S by TARSKI:def 4; ex z be Element of TA st F(z)=y & P[z] by A5,A14; hence x in A by A13,TARSKI:def 1; end; let x be set; assume x in A; then A15: {x} in S by A3,A4,A5; x in {x} by TARSKI:def 1; hence thesis by A15,TARSKI:def 4; end; hence thesis by A6,TOPS_2:26; end; end; Lm6: omega*`iC=iC proof omega c=iC by CARD_3:102; then A1: omega*`iC c=iC*`iC by CARD_3:136; iC*`iC=iC & iC c=omega*`iC by CARD_3:141,CARD_4:77; hence thesis by A1,XBOOLE_0:def 10; end; theorem Th14: for T st for F st F is open & F is Cover of T ex G st G c= F & G is Cover of T & card G c= C holds for A st A is closed & A is discrete holds card A c= C proof let T; assume A1: for F st F is open & F is Cover of T ex G st G c=F & G is Cover of T & card G c=C; set TOP=the topology of T; let A such that A2: A is closed and A3: A is discrete; defpred Q[set,set] means {$2}=$1/\A; A` in TOP by A2,PRE_TOPC:def 5; then A4: {A`}c=TOP by ZFMISC_1:37; defpred P[set,set] means A/\$2={$1}; A5: for x be set st x in A ex y be set st y in TOP & P[x,y] proof let x be set; assume x in A; then consider G be Subset of T such that A6: G is open & A/\G={x} by A3,TEX_2:32; take G; thus thesis by A6,PRE_TOPC:def 5; end; consider p be Function of A,TOP such that A7: for x be set st x in A holds P[x,p.x] from FUNCT_2:sch 1(A5); TOP is open by CANTOR_1:3; then reconsider RNG=rng p,AA={A`} as open Subset-Family of T by A4,TOPS_2:18,XBOOLE_1:1; reconsider RngA=RNG\/AA as open Subset-Family of T by TOPS_2:20; [#]T c=union RngA proof let x be set; assume A8: x in [#]T; per cases; suppose A9: x in A; dom p=A by FUNCT_2:def 1; then p.x in rng p by A9,FUNCT_1:def 5; 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 thesis by A10,TARSKI:def 4; end; suppose A11: not x in A; 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 thesis by A12,TARSKI:def 4; end; end; then RngA is Cover of T by SETFAM_1:def 12; then consider G be 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 be set st x in G\AA ex y be set st y in A & Q[x,y] proof let x be set; assume x in G\AA; 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 be set such that A17: y in dom p & p.y=x by FUNCT_1:def 5; take y; thus thesis by A7,A17; end; consider q be Function of G\AA,A such that A18: for x be set st x in G\AA holds Q[x,q.x] from FUNCT_2:sch 1(A16); per cases; suppose A is empty; hence thesis; end; suppose A is non empty; then A19: dom q=G\AA by FUNCT_2:def 1; A c=rng q proof let x be set such that A20: x in A; T is non empty by A20; then consider U be Subset of T such that A21: x in U and A22: U in G by A14,A20,PCOMPS_1:5; 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 5; x in A/\U by A20,A21,XBOOLE_0:def 4; hence thesis by A23,TARSKI:def 1; end; then A24: card A c=card(G\AA) by A19,CARD_1:28; card(G\AA)c=card G by CARD_1:27,XBOOLE_1:36; then card A c=card G by A24,XBOOLE_1:1; hence card A c=C by A15,XBOOLE_1:1; end; end; theorem Th15: for TM st for Am st Am is closed & Am is discrete holds card Am c= iC holds for Am st Am is discrete holds card Am c= iC proof let TM; assume A1: for Am st Am is closed & Am is discrete holds card Am c=iC; let Am such that A2: Am is discrete; per cases; suppose Am is empty; hence thesis; end; suppose A3: Am is non empty; then reconsider Tm=TM as metrizable(non empty TopSpace); Am c=Cl Am by PRE_TOPC:48; then reconsider ClA=Cl Am as non empty closed Subset of Tm by A3; set TA=TM|(Cl Am); set TA=Tm|ClA; reconsider A'=Am as open Subset of TA by A2,Th13; consider F be closed countable Subset-Family of TA such that A4: A'=union F by TOPGEN_4:def 6; consider f be Function of NAT,F such that A5: rng f=F by A3,A4,CARD_3:146,ZFMISC_1:2; A6: for x be set st x in dom f holds card(f.x)c=iC proof let x be set; assume x in dom f; then A7: f.x in rng f by FUNCT_1:def 5; then reconsider fx=f.x as Subset of TA by A5; A8: f.x c=Am by A4,A7,ZFMISC_1:92; then reconsider Fx=f.x as Subset of TM by XBOOLE_1:1; [#]TA=ClA & fx is closed by A7,PRE_TOPC:def 10,TOPS_2:def 2; then Fx is closed by TSEP_1:8; hence thesis by A1,A2,A8,TEX_2:28; end; card dom f=omega by A3,A4,CARD_1:84,FUNCT_2:def 1,ZFMISC_1:2; then card Union f c=(omega)*`iC by A6,CARD_3:132; hence thesis by A4,A5,Lm6; end; end; theorem Th16: for T st for A st A is discrete holds card A c= C for F st F is open & not {} in F & for A,B st A in F & B in F & A <> B holds A misses B holds card F c= C proof let T; assume A1: for A st A is discrete holds card A c=C; let F such that A2: F is open and A3: not{} in F and A4: for A,B st A in F & B in F & A<>B holds A misses B; per cases; suppose F is empty; hence thesis; end; suppose A5: F is non empty; deffunc P(set)=the Element of$1; A6: for x be set st x in F holds P(x) in [#]T proof let x be set; assume A7: x in F; then x<>{} by A3; then P(x) in x; hence thesis by A7; end; consider p be Function of F,[#]T such that A8: for x be set st x in F holds p.x=P(x) from FUNCT_2:sch 2(A6); reconsider RNG=rng p as Subset of T; ex xx be set st xx in F by A5,XBOOLE_0:def 1; then A9: T is non empty by A3; then A10: dom p=F by FUNCT_2:def 1; for x be Point of T st x in RNG ex G be Subset of T st G is open & RNG/\G={x} proof let x be Point of T; assume A11: x in RNG; then consider G be set such that A12: G in F and A13: p.G=x by A10,FUNCT_1:def 5; reconsider G as Subset of T by A12; A14: RNG/\G c={x} proof let y be set; assume A15: y in RNG/\G; then A16: y in G by XBOOLE_0:def 4; y in RNG by A15,XBOOLE_0:def 4; then consider z be set such that A17: z in F and A18: p.z=y by A10,FUNCT_1:def 5; y=P(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 thesis by TARSKI:def 1; end; take G; thus G is open by A2,A12,TOPS_2:def 1; x=P(G) by A8,A12,A13; then x in RNG/\G by A3,A11,A12,XBOOLE_0:def 4; hence thesis by A14,ZFMISC_1:39; end; then A19: card RNG c=C by A1,A9,TEX_2:37; for x1,x2 be set st x1 in dom p & x2 in dom p & p.x1=p.x2 holds x1=x2 proof let x1,x2 be set such that A20: x1 in dom p and A21: x2 in dom p and A22: p.x1=p.x2; A23: p.x1=P(x1) & x1<>{} by A3,A8,A20; p.x2=P(x2) & x2<>{} by A3,A8,A21; then x1 meets x2 by A22,A23,XBOOLE_0:3; hence thesis by A4,A10,A20,A21; end; then p is one-to-one by FUNCT_1:def 8; then card F c=card RNG by A10,CARD_1:26; hence thesis by A19,XBOOLE_1:1; end; end; theorem Th27: for F st F is Cover of T ex G st G c= F & G is Cover of T & card G c= card [#]T proof let F such that A1: F is Cover of T; per cases; suppose A2: F is empty; take F; thus thesis by A1,A2; end; suppose A3: F is non empty; defpred P[set,set] means $1 in $2; A4: for x be set st x in [#]T ex y be set st y in F & P[x,y] proof let x be set; assume x in [#]T; then x in union F by A1,SETFAM_1:60; then ex y be set st x in y & y in F by TARSKI:def 4; hence thesis; end; consider g be Function of[#]T,F such that A5: for x be set st x in [#]T holds P[x,g.x] from FUNCT_2:sch 1(A4); reconsider R=rng g as Subset-Family of T by XBOOLE_1:1; take R; A6: dom g=[#]T by A3,FUNCT_2:def 1; [#]T c=union R proof let x be set; assume x in [#]T; then x in g.x & g.x in R by A5,A6,FUNCT_1:def 5; hence thesis by TARSKI:def 4; end; hence thesis by A6,CARD_1:28,SETFAM_1:def 12; end; end; Lm7: (for Fm st Fm is open & not{} in Fm & for Am,Bm st Am in Fm & Bm in Fm & Am<>Bm holds Am misses Bm holds card Fm c=iC) implies density TM c=iC proof assume A1: for Fm st Fm is open & not{} in Fm & for Am,Bm st Am in Fm & Bm in Fm & Am<>Bm holds Am misses Bm holds card Fm c=iC; per cases; suppose A2: TM is empty; ex D be Subset of TM st D is dense & density TM=card D by TOPGEN_1:def 12; hence thesis by A2; end; suppose A3: TM is non empty; consider metr be 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 9; reconsider M=SpaceMetr(the carrier of TM,metr) as non empty MetrSpace by A3,A4,PCOMPS_1:40; defpred P[set,set] means for n be Nat st $1=n ex G be Subset of TM st G=$2 & card G c= iC & for p be Element of M ex q be 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:8; A7: for x be set st x in NAT ex y be set st y in bool the carrier of TM & P[x,y] proof let x be set; assume x in NAT; 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:13; then consider A be Subset of M such that A9: for p,q be Point of M st p<>q & p in A & q in A holds dist(p,q)>=r and A10: for p be Point of M ex q be 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 c=the topology of TM proof let x be set; assume x in BALL; then ex p be Point of M st x=Ball(p,r/2) & p in A; hence thesis by A5,PCOMPS_1:33; end; the topology of TM is open by CANTOR_1:3; then reconsider BALL as open Subset-Family of TM by A11,TOPS_2:18,XBOOLE_1:1; defpred Q[set,set] means for p be Point of M st Ball(p,r/2)=$1 & p in A holds p=$2; A12: for x be set st x in BALL ex y be set st y in A & Q[x,y] proof let x be set; assume x in BALL; then consider p be Point of M such that A13: x=Ball(p,r/2) and A14: p in A; A15: r/2B' holds A' misses B' proof let A',B' be Subset of TM such that A22: A' in BALL and A23: B' in BALL and A24: A'<>B'; consider b be Element of M such that A25: Ball(b,r/2)=B' and A26: b in A by A23; consider a be Element of M such that A27: Ball(a,r/2)=A' and A28: a in A by A22; assume A' meets B'; then consider x be set such that A29: x in A' and A30: x in B' by XBOOLE_0:3; reconsider x as Element of M by A27,A29; A31: dist(a,x)=r by A9,A24,A25,A26,A27,A28; hence thesis by A32,XXREAL_0:2; end; take RNG; thus RNG in bool the carrier of TM; let m be Nat such that A33: x=m; A34: now let p be Element of M; consider q be Point of M such that A35: q in A and A36: p in Ball(q,r) by A10; take q; 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 5,METRIC_1:12; end; not {} in BALL proof assume {} in BALL; then consider p be Element of M such that A38: Ball(p,r/2)={} and p in A; dist(p,p)=0 by METRIC_1:1; hence thesis by A8,A38,METRIC_1:12; end; then card BALL c=iC by A1,A21; hence thesis by A20,A34,XBOOLE_1:1; end; consider p be Function of NAT,bool the carrier of TM such that A39: for x be set st x in NAT holds P[x,p.x] from FUNCT_2:sch 1(A7); reconsider Up=Union p as Subset of TM; for U be Subset of TM st U<>{} & U is open holds Up meets U proof let U be Subset of TM; reconsider U'=U as Subset of M by A3,A4,PCOMPS_2:8; assume that A40: U<>{} and A41: U is open; consider q be set such that A42: q in U by A40,XBOOLE_0:def 1; reconsider q as Element of M by A3,A4,A42,PCOMPS_2:8; U' in Family_open_set(M) by A5,A41,PRE_TOPC:def 5; then consider r be Real such that A43: r>0 and A44: Ball(q,r)c=U' by A42,PCOMPS_1:def 5; consider n be Element of NAT such that A45: 1/(2|^n)<=r by A43,PREPOWER:106; consider G be Subset of TM such that A46: G=p.n and card G c=iC and A47: for p be Element of M ex q be Element of M st q in G & dist(p,q)<1/(2|^n) by A39; consider qq be Element of M such that A48: qq in G and A49: dist(q,qq)<1/(2|^n) by A47; dist(q,qq)0 and A14: Ball(p',r)c=B by A4,A11,A12,PCOMPS_1:def 5; consider n be Element of NAT such that A15: 1/(2|^n)<=r/2 by A13,PREPOWER:106; reconsider B2=Ball(p',1/(2|^n)) as Subset of TM by A2,A3,PCOMPS_2:8; 2|^n>0 & dist(p',p')=0 by METRIC_1:1,PREPOWER:13; then A16: p' in B2 by METRIC_1:12; B2 in TOP by A4,PCOMPS_1:33; then B2 is open by PRE_TOPC:def 5; then B2 meets Am by A1,A16,TOPS_1:80; then consider q be set such that A17: q in B2 and A18: q in Am by XBOOLE_0:3; reconsider q as Point of Tm by A17; reconsider B3=Ball(q,1/(2|^n)) as Subset of TM by A2,A3,PCOMPS_2:8; take B3; 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:25; A19: dist(p',q)<1/(2|^n) by A17,METRIC_1:12; hence p in B3 by METRIC_1:12; let y be set; assume A20: y in B3; then reconsider t=y as Point of Tm; dist(q,t)<1/(2|^n) by A20,METRIC_1:12; then A21: dist(q,t) (c) theorem Th18: weight TM c= iC iff for Fm st Fm is open & Fm is Cover of TM ex Gm st Gm c=Fm & Gm is Cover of TM & card Gm c= iC proof hereby assume A1: weight TM c=iC; let F be Subset-Family of TM such that A2: F is open and A3: F is Cover of TM; per cases; suppose A4: TM is empty; reconsider G={} as Subset-Family of TM by TOPGEN_4:18; take G; the carrier of TM = {} by A4; then [#]TM=union G by A4; hence G c=F & G is Cover of TM & card G c=iC by SETFAM_1:def 12,XBOOLE_1:2; end; suppose TM is non empty; then consider G be open Subset-Family of TM such that A5: G c=F & union G=union F & card G c=weight TM by A2,TOPGEN_2:12; reconsider G as Subset-Family of TM; take G; union F=[#]TM by A3,SETFAM_1:60; hence G c=F & G is Cover of TM & card G c=iC by A1,A5,SETFAM_1:def 12,XBOOLE_1:1; end; end; assume for F be Subset-Family of TM st F is open & F is Cover of TM ex G be Subset-Family of TM st G c=F & G is Cover of TM & card G c=iC; then for A be Subset of TM st A is closed & A is discrete holds card A c=iC by Th14; then for A be Subset of TM st A is discrete holds card A c=iC by Th15; then for F be Subset-Family of TM st F is open & not{} in F & for A,B be Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c=iC by Th16; then density TM c=iC by Lm7; hence thesis by Lm8; end; :: General Topology Th 4.1.15 (a) <=> (d) theorem Th19: weight TM c=iC iff for Am st Am is closed & Am is discrete holds card Am c= iC proof hereby assume weight TM c=iC; then for Fm st Fm is open & Fm is Cover of TM ex Gm st Gm c=Fm & Gm is Cover of TM & card Gm c=iC by Th18; hence for Am st Am is closed & Am is discrete holds card Am c=iC by Th14; end; assume for Am st Am is closed & Am is discrete holds card Am c=iC; then for Am st Am is discrete holds card Am c=iC by Th15; then for Fm st Fm is open & not{} in Fm & for Am,Bm st Am in Fm & Bm in Fm & Am<>Bm holds Am misses Bm holds card Fm c=iC by Th16; then density TM c=iC by Lm7; hence thesis by Lm8; end; :: General Topology Th 4.1.15 (a) <=> (e) theorem Th20: weight TM c= iC iff for Am st Am is discrete holds card Am c= iC proof hereby assume weight TM c=iC; then for A be Subset of TM st A is closed & A is discrete holds card A c=iC by Th19; hence for A be Subset of TM st A is discrete holds card A c=iC by Th15; end; assume for A be Subset of TM st A is discrete holds card A c=iC; then for F be Subset-Family of TM st F is open & not{} in F & for A,B be Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c=iC by Th16; then density TM c=iC by Lm7; hence thesis by Lm8; end; :: General Topology Th 4.1.15 (a) <=> (f) theorem Th21: weight TM c= iC iff for Fm st Fm is open & not{} in Fm & for Am,Bm st Am in Fm & Bm in Fm & Am <> Bm holds Am misses Bm holds card Fm c= iC proof hereby assume weight TM c=iC; then for A be Subset of TM st A is discrete holds card A c=iC by Th20; hence for F be Subset-Family of TM st F is open & not{} in F & for A,B be Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c= iC by Th16; end; assume for F be Subset-Family of TM st F is open & not{} in F & for A,B be Subset of TM st A in F & B in F & A<>B holds A misses B holds card F c=iC; then density TM c=iC by Lm7; hence thesis by Lm8; end; :: General Topology Th 4.1.15 (a) <=> (g) theorem Th22: weight TM c= iC iff density TM c= iC proof consider A be Subset of TM such that A1: A is dense and A2: density TM=card A by TOPGEN_1:def 12; hereby assume weight TM c=iC; then for F be Subset-Family of TM st F is open & not{} in F & for A,B be 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 Lm7; end; assume density TM c=iC; then A3: omega*`card A c=omega*`iC by A2,CARD_3:136; weight TM c=omega*`card A by A1,Th17; then weight TM c=omega*`iC by A3,XBOOLE_1:1; hence thesis by Lm6; end; theorem Th23: for B be Basis of TM st for Fm st Fm is open & Fm is Cover of TM ex Gm st Gm c=Fm & Gm is Cover of TM & card Gm c= iC ex underB be Basis of TM st underB c= B & card underB c= iC proof let B be Basis of TM such that A1: for F being Subset-Family of TM st F is open & F is Cover of TM ex G be Subset-Family of TM st G c=F & G is Cover of TM & card G c=iC; per cases; suppose TM is empty; then weight TM=0; then consider underB be Basis of TM such that A2: card underB=0 by WAYBEL23:75; take underB; underB={} by A2; hence thesis by XBOOLE_1:2; end; suppose A3: TM is non empty; set TOP=the topology of TM,cT=the carrier of TM; consider metr be Function of[:cT,cT:],REAL such that A4: metr is_metric_of cT and A5: Family_open_set(SpaceMetr(cT,metr))=TOP by PCOMPS_1:def 9; reconsider Tm=SpaceMetr(cT,metr) as non empty MetrSpace by A3,A4,PCOMPS_1:40; defpred P[set,set] means for n be Nat st $1=n ex G be open Subset-Family of TM st G c={U where U is Subset of TM: U in B & ex p be 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= TOP by CANTOR_1:def 2; A7: for x be set st x in NAT ex y be set st P[x,y] proof let x be set; assume x in NAT; then reconsider n=x as Nat; set F={U where U is Subset of TM:U in B & ex p be Element of Tm st U c=Ball (p,1/(2|^n))}; A8: F c=TOP proof let f be set; assume f in F; then ex U be Subset of TM st f=U & U in B & ex p be Point of Tm st U c= Ball(p,1/(2|^n)); hence thesis by A6; end; then reconsider F as Subset-Family of TM by XBOOLE_1:1; reconsider F as open Subset-Family of TM by A8,CANTOR_1:3,TOPS_2:18; cT c=union F proof let y be set; assume A9: y in cT; then reconsider p=y as Point of TM; reconsider q=y as Element of Tm by A3,A4,A9,PCOMPS_2:8; 2|^n>0 & dist(q,q)=0 by METRIC_1:1,NEWTON:102; then A10: q in Ball(q,1/(2|^n)) by METRIC_1:12; reconsider BALL=Ball(q,1/(2|^n)) as Subset of TM by A3,A4,PCOMPS_2:8; BALL in Family_open_set(Tm) by PCOMPS_1:33; then BALL is open by A5,PRE_TOPC:def 5; then consider U be 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 thesis by A12,TARSKI:def 4; end; then F is Cover of TM by SETFAM_1:def 12; then consider G be 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; let m be Nat; assume A16: x=m; G is open by A14,TOPS_2:18; hence thesis by A14,A15,A16; end; consider f be Function such that A17: dom f=NAT & for e be set st e in NAT holds P[e,f.e] from CLASSES1:sch 1(A7); A18: union rng f c=B proof let b be set; assume b in union rng f; then consider y be set such that A19: b in y and A20: y in rng f by TARSKI:def 4; consider x be set such that A21: x in dom f and A22: f.x=y by A20,FUNCT_1:def 5; reconsider n=x as Nat by A17,A21; ex G be open Subset-Family of TM st G c={U where U is Subset of TM:U in B & ex p be 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 be Point of Tm st U c= Ball(p,1/(2|^n))} by A19,A22; then ex U be Subset of TM st U=b & U in B & ex p be Point of Tm st U c=Ball(p,1/(2|^n)); hence thesis; end; then reconsider Urngf=union rng f as Subset-Family of TM by XBOOLE_1:1; for A be Subset of TM st A is open for p be Point of TM st p in A ex a be Subset of TM st a in Urngf & p in a & a c=A proof let A be Subset of TM such that A23: A is open; A24: A in Family_open_set(Tm) by A5,A23,PRE_TOPC:def 5; let p be Point of TM such that A25: p in A; reconsider p'=p as Element of Tm by A3,A4,PCOMPS_2:8; consider r be Real such that A26: r>0 and A27: Ball(p',r)c=A by A24,A25,PCOMPS_1:def 5; consider n be Element of NAT such that A28: 1/(2|^n)<=r/2 by A26,PREPOWER:106; consider G be open Subset-Family of TM such that A29: G c={U where U is Subset of TM:U in B & ex p be Point of Tm st U c= Ball(p,1/(2|^n))} and A30: G is Cover of TM and card G c=iC and A31: f.n=G by A17; [#]TM=union G by A30,SETFAM_1:60; then consider a be set such that A32: p in a and A33: a in G by A3,TARSKI:def 4; a in {U where U is Subset of TM:U in B & ex p be Point of Tm st U c=Ball(p,1/(2|^n))} by A29,A33; then consider U be Subset of TM such that A34: a=U and U in B and A35: ex p be Point of Tm st U c=Ball(p,1/(2|^n)); take U; f.n in rng f by A17,FUNCT_1:def 5; hence U in Urngf & p in U by A31,A32,A33,A34,TARSKI:def 4; thus U c=A proof let u' be set; consider pp be Element of Tm such that A36: U c=Ball(pp,1/(2|^n)) by A35; assume A37: u' in U; then reconsider u=u' as Element of Tm by A3,A4,PCOMPS_2:8; dist(pp,u)<1/(2|^n) by A36,A37,METRIC_1:12; then A38: dist(pp,u) < r/2 by A28,XXREAL_0:2; dist(pp,p')<1/(2|^n) by A32,A34,A36,METRIC_1:12; then dist(p',pp) (a) Th25: TM is Lindelof iff TM is second-countable proof hereby assume TM is Lindelof; then for F be Subset-Family of TM st F is open & F is Cover of TM ex G be Subset-Family of TM st G c=F & G is Cover of TM & card G c=omega by Lm9; then weight TM c=omega by Th18; hence TM is second-countable by WAYBEL23:def 6; end; assume TM is second-countable; then weight TM c=omega by WAYBEL23:def 6; then for F be Subset-Family of TM st F is open & F is Cover of TM ex G be Subset-Family of TM st G c=F & G is Cover of TM & card G c=omega by Th18; hence thesis by Lm9; end; registration cluster Lindelof -> second-countable (metrizable TopSpace); coherence by Th25; end; :: General Topology Cor 4.1.16 (b) <=> (c) Th26: TM is Lindelof iff TM is separable proof hereby assume TM is Lindelof; 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; end; assume TM is separable; 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 thesis by Th25; end; registration cluster Lindelof -> separable (metrizable TopSpace); coherence by Th26; cluster separable -> Lindelof (metrizable TopSpace); coherence by Th26; end; registration cluster Lindelof metrizable (non empty TopSpace); existence proof set X=the non empty finite set; TopSpaceMetr DiscreteSpace X is finite; hence thesis; end; :: General Topology Th 3.8.1 cluster second-countable -> Lindelof TopSpace; coherence proof let T be TopSpace; assume A1: T is second-countable; let F be Subset-Family of T such that A2: F is open and A3: F is Cover of T; per cases; suppose A4: T is empty; take F; F c={{}} proof let x be set; assume x in F; then x={} by A4; hence thesis by TARSKI:def 1; end; hence thesis by A3; end; suppose T is non empty; hence thesis by A1,A2,A3,COMPL_SP:34; end; end; :: General Topology Th 3.8.2 cluster regular Lindelof -> normal TopSpace; coherence proof let T be TopSpace; assume that A5: T is regular and A6: T is Lindelof; per cases; suppose A7: T is empty; let F1,F2 be Subset of T such that F1 is closed and F2 is closed and A8: F1 misses F2; take F1,F2; thus thesis by A7,A8; end; suppose A9: T is non empty; set TOP=the topology of T; for A be Subset of T,U be open Subset of T st A is closed & U is open & A c= U ex W be Function of NAT,bool(the carrier of T) st A c=Union W & Union W c= U & for n be Element of NAT holds Cl(W.n)c=U & W.n is open proof let A be Subset of T,U be open Subset of T such that A10: A is closed and U is open and A11: A c=U; defpred P[set,set] means for p be Point of T st p=$1 ex W be Subset of T st W is open & p in W & Cl W c=U & $2=W; A12: for x be set st x in A ex y be set st y in TOP & P[x,y] proof let x be set; assume A13: x in A; then reconsider p=x as Point of T; U=U``; then consider G1,G2 be 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 17; take G1; thus G1 in TOP by A14,PRE_TOPC:def 5; G1 c=G2` by A18,SUBSET_1:43; then A20: Cl G1 c=Cl(G2`) by PRE_TOPC:49; let q be Point of T such that A21: q=x; Cl(G2`)=G2` & G2`c=U by A15,A17,PRE_TOPC:52,SUBSET_1:36; hence thesis by A14,A16,A20,A21,XBOOLE_1:1; end; consider w be Function of A,TOP such that A22: for x be set st x in A holds P[x,w.x] from FUNCT_2:sch 1(A12); A` in TOP by A10,PRE_TOPC:def 5; then TOP is open & {A`}c=TOP by CANTOR_1:3,ZFMISC_1:37; then reconsider RNG=rng w,AA={A`} as open Subset-Family of T by TOPS_2:18,XBOOLE_1:1; set RngA=RNG\/AA; A23: dom w=A by FUNCT_2:def 1; [#]T c=union RngA proof let x be set; assume A24: x in [#]T; then reconsider p=x as Point of T; per cases; suppose A25: x in A; then consider W be Subset of T such that W is open and A26: x in W and Cl W c=U and A27: w.x=W by A22; W in rng w by A23,A25,A27,FUNCT_1:def 5; then W in RngA by XBOOLE_0:def 3; hence thesis by A26,TARSKI:def 4; end; suppose A28: not x in A; A` in AA by TARSKI:def 1; then A29: A` in RngA by XBOOLE_0:def 3; x in A` by A24,A28,XBOOLE_0:def 5; hence thesis by A29,TARSKI:def 4; end; end; then RngA is open Subset-Family of T & RngA is Cover of T by SETFAM_1:def 12,TOPS_2:20; then consider G be Subset-Family of T such that A30: G c=RngA and A31: G is Cover of T and A32: G is countable by A6,Def2; A33: [#]T=union G by A31,SETFAM_1:60; per cases; suppose G\AA is empty; then G c=AA by XBOOLE_1:37; then A34: union G c=union AA by ZFMISC_1:95; take W=(NAT-->{}T); rng W={{}T} by FUNCOP_1:14; then A35: ({}T)`=[#]T & Union W={}T by ZFMISC_1:31; union AA=A` by ZFMISC_1:31; then A`=[#]T by A33,A34,XBOOLE_0:def 10; hence A c=Union W & Union W c=U by A35,SUBSET_1:64,XBOOLE_1:2; let n be Element of NAT; W.n={}T by FUNCOP_1:13; then Cl(W.n)={}T by PRE_TOPC:52; hence thesis by FUNCOP_1:13,XBOOLE_1:2; end; suppose A36: G\AA is non empty; G\AA is countable by A32,CARD_3:130; then consider W be Function of NAT,G\AA such that A37: rng W=G\AA by A36,CARD_3:146; reconsider W as Function of NAT,bool(the carrier of T) by A36,A37,FUNCT_2:8; take W; thus A c=Union W proof let x be set; assume A38: x in A; then consider y be set such that A39: x in y and A40: y in G by A33,TARSKI:def 4; not x in A` by A38,XBOOLE_0:def 5; then not y in AA by A39,TARSKI:def 1; then y in rng W by A37,A40,XBOOLE_0:def 5; then ex n be set st n in dom W & W.n=y by FUNCT_1:def 5; hence thesis by A39,PROB_1:25; end; A41: dom W=NAT by FUNCT_2:def 1; thus Union W c=U proof let x be set; assume x in Union W; then consider n be Element of NAT such that A42: x in W.n by PROB_1:25; A43: W.n in G\AA by A37,A41,FUNCT_1:def 5; then W.n in G by ZFMISC_1:64; then A44: W.n in RNG or W.n in AA by A30,XBOOLE_0:def 3; W.n<>A` by A43,ZFMISC_1:64; then consider xx be set such that A45: xx in dom w & w.xx=W.n by A44,FUNCT_1:def 5,TARSKI:def 1; consider W' be Subset of T such that W' is open and xx in W' and A46: Cl W' c=U and A47: W.n=W' by A22,A23,A45; W' c=Cl W' by PRE_TOPC:48; then x in Cl W' by A42,A47; hence thesis by A46; end; let n be Element of NAT; A48: W.n in G\AA by A37,A41,FUNCT_1:def 5; then W.n in G by ZFMISC_1:64; then A49: W.n in RNG or W.n in AA by A30,XBOOLE_0:def 3; W.n<>A` by A48,ZFMISC_1:64; then consider xx be set such that A50: xx in dom w & w.xx=W.n by A49,FUNCT_1:def 5,TARSKI:def 1; ex W' be Subset of T st W' is open & xx in W' & Cl W' c=U & W.n=W' by A22,A23,A50; hence thesis; end; end; hence thesis by A9,NAGATA_1:18; end; end; cluster countable -> Lindelof TopSpace; coherence proof let T be TopSpace; assume T is countable; then [#]T is countable by ORDERS_4:def 2; then A51: card[#]T c=omega by CARD_3:def 15; let F be Subset-Family of T; assume that F is open and A52: F is Cover of T; consider G be Subset-Family of T such that A53: G c=F & G is Cover of T and A54: card G c=card[#]T by A52,Th27; take G; card G c=omega by A54,A51,XBOOLE_1:1; hence thesis by A53,CARD_3:def 15; end; end; Lm10: the TopStruct of TOP-REAL 1 is second-countable proof reconsider R=RAT as Subset of R^1 by NUMBERS:12,TOPMETR:24; Y: the TopStruct of TOP-REAL 1 = TopSpaceMetr Euclid 1 & the TopStruct of TOP-REAL (1+1) = TopSpaceMetr Euclid (1+1) by EUCLID:def 8; X: weight [:the TopStruct of TOP-REAL 1, the TopStruct of TOP-REAL 1:] = weight the TopStruct of TOP-REAL 2 by Th4,Y,TOPREAL7:27; K:the TopStruct of [:R^1,R^1:], the TopStruct of TOP-REAL 2 are_homeomorphic by TOPREALA:36,TOPREAL6:86; A1: weight the TopStruct of [:R^1,R^1:] = weight the TopStruct of TOP-REAL 2 by Th4,K; Cl R=[#](R^1) by BORSUK_5:35; 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 WAYBEL23:def 6,TOPMETR:def 7; weight (the TopStruct of TOP-REAL 1) c= weight [:the TopStruct of TOP-REAL 1,the TopStruct of TOP-REAL 1:] by Th6; then weight (the TopStruct of TOP-REAL 1) c= omega by X,A2,A1,XBOOLE_1:1; hence thesis by WAYBEL23:def 6; end; registration let n be Nat; cluster the TopStruct of TOP-REAL n -> second-countable; coherence proof defpred P[Nat] means the TopStruct of TOP-REAL $1 is second-countable; A1: for n be Nat st P[n] holds P[n+1] proof let n be Nat; Y: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n & the TopStruct of TOP-REAL 1 = TopSpaceMetr Euclid 1 & the TopStruct of TOP-REAL (n+1) = TopSpaceMetr Euclid (n+1) by EUCLID:def 8; n in NAT by ORDINAL1:def 13; then A2: weight [:the TopStruct of TOP-REAL n, the TopStruct of TOP-REAL 1:] = weight the TopStruct of TOP-REAL(n+1) by Th4,Y,TOPREAL7:27; assume P[n]; then weight [:the TopStruct of TOP-REAL n, the TopStruct of TOP-REAL 1:] c= omega by Lm10,WAYBEL23:def 6; hence thesis by A2,WAYBEL23:def 6; end; [#](TOP-REAL 0) = REAL 0 by EUCLID:25 .= 0-tuples_on REAL by EUCLID:def 1 .= {<*>REAL} by FINSEQ_2:112; then the TopStruct of TOP-REAL 0 is finite; then A3: P[0]; for n be Nat holds P[n] from NAT_1:sch 2(A3,A1); hence thesis; end; end; registration let T be Lindelof TopSpace; let A be closed Subset of T; :: General Topology Cor 3.8.4 cluster T|A -> Lindelof; coherence proof set TOP=the topology of T; let FA be Subset-Family of T|A such that A1: FA is open and A2: FA is Cover of T|A; defpred P[set,set] means $2/\A=$1; A3: for x be set st x in FA ex y be set st y in TOP & P[x,y] proof let x be set such that A4: x in FA; 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 5; then consider Q be Subset of T such that A5: Q in TOP & X=Q/\[#](T|A) by PRE_TOPC:def 9; take Q; thus thesis by A5,PRE_TOPC:def 10; end; consider f be Function of FA,TOP such that A6: for x be set st x in FA holds P[x,f.x] from FUNCT_2:sch 1(A3); A` in TOP by PRE_TOPC:def 5; then TOP is open & {A`}c=TOP by CANTOR_1:3,ZFMISC_1:37; then reconsider RNG=rng f,AA={A`} as open Subset-Family of T by TOPS_2:18,XBOOLE_1:1; reconsider RA=RNG\/AA as open Subset-Family of T by TOPS_2:20; A7: A = [#](T|A) by PRE_TOPC:def 10; A8: dom f = FA by FUNCT_2:def 1; [#]T c=union RA proof A9: A\/(A`)=[#](the carrier of T) by SUBSET_1:25; let x be set such that A10: x in [#]T; per cases by A9,A10,XBOOLE_0:def 3; suppose A11: x in A; A=union FA by A2,A7,SETFAM_1:60; then consider y be 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 5; 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 thesis by A14,TARSKI:def 4; end; suppose A15: x in A`; A` in AA by TARSKI:def 1; then A` in RA by XBOOLE_0:def 3; hence thesis by A15,TARSKI:def 4; end; end; then RA is Cover of T by SETFAM_1:def 12; then consider G be Subset-Family of T such that A16: G c=RA and A17: G is Cover of T and A18: G is countable by Def2; reconsider E={{}} as Subset-Family of T|A by SETFAM_1:61; A19: card G c=omega by A18,CARD_3:def 15; set GA=G|A; take GE=GA\E; thus GE c=FA proof let x be set; assume A20: x in GE; then A21: x<>{} by ZFMISC_1:64; x in GA by A20,ZFMISC_1:64; then consider R be Subset of T such that A22: R in G and A23: R /\ A = x by TOPS_2:def 3; per cases by A16,A22,XBOOLE_0:def 3; suppose R in RNG; then consider y be set such that A24: y in dom f and A25: f.y=R by FUNCT_1:def 5; y=R/\A by A6,A24,A25; hence thesis by A23,A24; end; suppose R in AA; then R=A` by TARSKI:def 1; then x=A\A by A23,SUBSET_1:32; hence thesis by A21,XBOOLE_1:37; end; end; union G=[#]T by A17,SETFAM_1:60; then [#](T|A) = union GA by A7,TOPS_2:43 .= union GE by PARTIT1:3; hence GE is Cover of T|A by SETFAM_1:def 12; card GA c=card G by Th7; then card GA c=omega by A19,XBOOLE_1:1; then GA is countable by CARD_3:def 15; hence thesis by CARD_3:130; end; end; registration let TM be Lindelof metrizable TopSpace; let A be Subset of TM; cluster TM|A -> Lindelof; coherence; end; definition let T; let A,B,L be Subset of T; pred L separates A,B means :Def3: ex U,W be open Subset of T st A c=U & B c=W & U misses W & L=(U\/W)`; end; Lm11: for M be non empty MetrSpace for A,B be 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; set TM=TopSpaceMetr M; let A,B be non empty Subset of TM; set dA=dist_min A; set dB=dist_min B; consider g be Function of the carrier of TM,the carrier of(R^1) such that A1: for p be Point of TM,r1,r2 be real number st dA.p=r1 & dB.p=r2 holds g.p=r1-r2 and A2: g is continuous by JGRAPH_2:31; reconsider A=].-infty,0.[ as Subset of R^1 by TOPMETR:24; set gA={p where p is Point of TM:dA.p-dB.p<0}; A3: [#]R^1={} implies [#]TM={}; A4: g"A c=gA proof let x be set; assume A5: x in g"A; then reconsider p=x as Point of TM; A6: dA.p-dB.p=g.x by A1; g.x in A by A5,FUNCT_1:def 13; then dA.p-dB.p<0 by A6,XXREAL_1:233; hence thesis; end; A7: gA c=g"A proof let x be set; assume x in gA; then consider p be Point of TM such that A8: p=x and A9: dA.p-dB.p<0; g.p=dA.p-dB.p by A1; then dom g=[#]TM & g.p in A by A9,FUNCT_2:def 1,XXREAL_1:233; hence thesis by A8,FUNCT_1:def 13; end; A is open by BORSUK_5:63; then g"A is open by A2,A3,TOPS_2:55; hence thesis by A4,A7,XBOOLE_0:def 10; end; Lm12: for A,B be Subset of TM st A,B are_separated ex U,W be open Subset of TM st A c=U & B c=W & U misses W proof let A,B be Subset of TM such that A1: A,B are_separated; set TOP=the topology of TM,cTM=the carrier of TM; consider metr be Function of[:cTM,cTM:],REAL such that A2: metr is_metric_of cTM and A3: Family_open_set(SpaceMetr(cTM,metr))=TOP by PCOMPS_1:def 9; per cases; suppose A4: A={}TM; take U={}TM,W=[#]TM; thus thesis by A4,XBOOLE_1:65; end; suppose A5: B={}TM; take U=[#]TM,W={}TM; thus thesis by A5,XBOOLE_1:65; end; suppose A6: A<>{}TM & B<>{}TM; then A7: TM is non empty; then reconsider Tm=SpaceMetr(cTM,metr) as non empty MetrSpace by A2,PCOMPS_1:40; set TTm=TopSpaceMetr Tm; reconsider A'=A,B'=B as Subset of TTm by A2,A7,PCOMPS_2:8; set dA=dist_min A',dB=dist_min B'; reconsider U={p where p is Point of Tm:dA.p-dB.p<0}, W={p where p is Point of Tm:dB.p-dA.p<0} as open Subset of TTm by A6,Lm11; U in Family_open_set(Tm) & W in Family_open_set(Tm) by PRE_TOPC:def 5; then reconsider U,W as open Subset of TM by A3,PRE_TOPC:def 5; take U,W; A8: [#]TM=[#]TTm by A2,A7,PCOMPS_2:8; thus A c=U proof let x be set; assume A9: x in A; then reconsider p=x as Point of Tm by A2,A7,PCOMPS_2:8; A10: dA.p=0 by A9,HAUSDORF:5; 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 B' by A3,A8,TOPS_3:80; then A11: dB.p<>0 by A6,HAUSDORF:10; dB.p>=0 by A6,JORDAN1K:9; then dA.p-dB.p<0 by A11,A10; hence thesis; end; thus B c=W proof let x be set; assume A12: x in B; then reconsider p=x as Point of Tm by A2,A7,PCOMPS_2:8; A13: dB.p=0 by A12,HAUSDORF:5; 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 A' by A3,A8,TOPS_3:80; then A14: dA.p<>0 by A6,HAUSDORF:10; dA.p>=0 by A6,JORDAN1K:9; then dB.p-dA.p<0 by A14,A13; hence thesis; end; thus U misses W proof assume U meets W; then consider x be set such that A15: x in U and A16: x in W by XBOOLE_0:3; consider p be Point of Tm such that A17: p=x and A18: dB.p-dA.p<0 by A16; ex q be Point of Tm st q=x & dA.q-dB.q<0 by A15; then -(dA.p-dB.p)>-0 by A17; hence thesis by A18; end; end; end; :: Teoria wymiaru Lm 1.2.8 theorem Am,Bm are_separated implies ex L be Subset of TM st L separates Am,Bm proof assume Am,Bm are_separated; then consider U,W be open Subset of TM such that A1: Am c=U & Bm c=W & U misses W by Lm12; take L=(U\/W)`; thus thesis by A1,Def3; end; :: Teoria wymiaru Lm 1.2.9 theorem for M be Subset of TM, A1,A2 be closed Subset of TM, V1,V2 be open Subset of TM st A1 c=V1 & A2 c=V2 & Cl V1 misses Cl V2 for mV1,mV2,mL be Subset of TM|M st mV1 = M/\Cl V1 & mV2 = M/\Cl V2 & mL separates mV1,mV2 ex L be Subset of TM st L separates A1,A2 & M/\L c= mL proof let M be Subset of TM,A1,A2 be closed Subset of TM,V1,V2 be open Subset of TM such that A1: A1 c=V1 and A2: A2 c=V2 and A3: Cl V1 misses Cl V2; set TMM=TM|M; let mV1,mV2,mL be Subset of TMM such that A4: mV1=M/\Cl V1 and A5: mV2=M/\Cl V2 and A6: mL separates mV1,mV2; A7: V1/\M c=mV1 by A4,PRE_TOPC:48,XBOOLE_1:26; consider U',W' be open Subset of TMM such that A8: mV1 c=U' and A9: mV2 c=W' and A10: U' misses W' and A11: mL=(U'\/W')` by A6,Def3; A12: [#]TMM=M by PRE_TOPC:def 10; then reconsider u=U',w=W' as Subset of TM by XBOOLE_1:1; set u1=u\/A1,w1=w\/A2; A13: mV1/\w c=U'/\W' by A8,XBOOLE_1:26; U',W' are_separated by A10,TSEP_1:41; then A14: u,w are_separated by CONNSP_1:6; V1/\w = V1/\(M/\w) by A12,XBOOLE_1:28 .= V1/\M/\w by XBOOLE_1:16; then V1/\w c=mV1/\w by A7,XBOOLE_1:26; then V1/\w c=U'/\W' by A13,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 A15: V1 misses Cl w by TSEP_1:40; A16: Cl w1 misses u1 proof assume Cl w1 meets u1; then consider x be set such that A17: x in Cl w1 & x in u1 by XBOOLE_0:3; A18: Cl w1=(Cl w)\/Cl A2 by PRE_TOPC:50; per cases by A17,A18,XBOOLE_0:def 3; suppose x in Cl w & x in u; then Cl w meets u by XBOOLE_0:3; hence contradiction by A14,CONNSP_1:def 1; end; suppose x in Cl w & x in A1; hence contradiction by A1,A15,XBOOLE_0:3; end; suppose A19: x in Cl A2 & x in u; Cl A2 c=Cl V2 by A2,PRE_TOPC:49; then x in mV2 by A5,A12,A19,XBOOLE_0:def 4; hence contradiction by A9,A10,A19,XBOOLE_0:3; end; suppose A20: x in Cl A2 & x in A1; A21: Cl A2 c=Cl V2 & V1 c=Cl V1 by A2,PRE_TOPC:48,49; x in V1 by A1,A20; hence thesis by A3,A20,A21,XBOOLE_0:3; end; end; A22: V2/\M c=mV2 by A5,PRE_TOPC:48,XBOOLE_1:26; A23: mV2/\u c=U'/\W' by A9,XBOOLE_1:26; V2/\u = V2/\(M/\u) by A12,XBOOLE_1:28 .= V2/\M/\u by XBOOLE_1:16; then V2/\u c=mV2/\u by A22,XBOOLE_1:26; then V2/\u c=U'/\W' by A23,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 A24: V2 misses Cl u by TSEP_1:40; Cl u1 misses w1 proof assume Cl u1 meets w1; then consider x be set such that A25: x in Cl u1 & x in w1 by XBOOLE_0:3; A26: Cl u1=(Cl u)\/Cl A1 by PRE_TOPC:50; per cases by A25,A26,XBOOLE_0:def 3; suppose x in Cl u & x in w; then w meets Cl u by XBOOLE_0:3; hence contradiction by A14,CONNSP_1:def 1; end; suppose x in Cl u & x in A2; hence contradiction by A2,A24,XBOOLE_0:3; end; suppose A27: x in Cl A1 & x in w; Cl A1 c=Cl V1 by A1,PRE_TOPC:49; then x in mV1 by A4,A12,A27,XBOOLE_0:def 4; hence contradiction by A8,A10,A27,XBOOLE_0:3; end; suppose A28: x in Cl A1 & x in A2; A29: Cl A1 c=Cl V1 & V2 c=Cl V2 by A1,PRE_TOPC:48,49; x in V2 by A2,A28; hence thesis by A3,A28,A29,XBOOLE_0:3; end; end; then u1,w1 are_separated by A16,CONNSP_1:def 1; then consider U1,W1 be open Subset of TM such that A30: u1 c=U1 and A31: w1 c=W1 and A32: U1 misses W1 by Lm12; take L=(U1\/W1)`; A1 c=u1 by XBOOLE_1:7; then A33: A1 c=U1 by A30,XBOOLE_1:1; u c=u1 by XBOOLE_1:7; then A34: u c=U1 by A30,XBOOLE_1:1; w c=w1 by XBOOLE_1:7; then w c=W1 by A31,XBOOLE_1:1; then A35: u\/w c=U1\/W1 by A34,XBOOLE_1:13; A2 c=w1 by XBOOLE_1:7; then A2 c=W1 by A31,XBOOLE_1:1; hence L separates A1,A2 by A32,A33,Def3; A36: ([#]TMM)\(U'\/W') = 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\(U'\/W') by A35,XBOOLE_1:34; hence thesis by A36,PRE_TOPC:def 10; end;