:: 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;