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 )
per cases ( TM is empty or not TM is empty ) ;
suppose A4: 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; :: 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; :: 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