let M be non empty MetrSpace; :: thesis: ( M is compact iff for F being Subset-Family of st F is being_ball-family & F is Cover of holds
ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) )
thus ( M is compact implies for F being Subset-Family of st F is being_ball-family & F is Cover of holds
ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) ) :: thesis: ( ( for F being Subset-Family of st F is being_ball-family & F is Cover of holds
ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) ) implies M is compact )
proof
set TM = TopSpaceMetr M;
assume M is compact ; :: thesis: for F being Subset-Family of st F is being_ball-family & F is Cover of holds
ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite )
then A1: TopSpaceMetr M is compact by Def6;
let F be Subset-Family of ; :: thesis: ( F is being_ball-family & F is Cover of implies ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) )
reconsider TF = F as Subset-Family of by Th16;
assume that
A2: F is being_ball-family and
A3: F is Cover of ; :: thesis: ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite )
A4: TF is open
proof
let P be Subset of ; :: according to TOPS_2:def 1 :: thesis: ( not P in TF or P is open )
reconsider P' = P as Subset of by Th16;
assume P in TF ; :: thesis: P is open
then ex p being Point of ex r being Real st P' = Ball p,r by A2, Def4;
hence P is open by Th21; :: thesis: verum
end;
the carrier of M c= union F by A3, SETFAM_1:def 12;
then the carrier of (TopSpaceMetr M) c= union TF by Th16;
then TF is Cover of by SETFAM_1:def 12;
then consider TG being Subset-Family of such that
A5: TG c= TF and
A6: TG is Cover of and
A7: TG is finite by A1, A4, COMPTS_1:def 3;
reconsider G = TG as Subset-Family of by Th16;
take G ; :: thesis: ( G c= F & G is Cover of & G is finite )
the carrier of (TopSpaceMetr M) c= union TG by A6, SETFAM_1:def 12;
then the carrier of M c= union G by Th16;
hence ( G c= F & G is Cover of & G is finite ) by A5, A7, SETFAM_1:def 12; :: thesis: verum
end;
thus ( ( for F being Subset-Family of st F is being_ball-family & F is Cover of holds
ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) ) implies M is compact ) :: thesis: verum
proof
set TM = TopSpaceMetr M;
assume A8: for F being Subset-Family of st F is being_ball-family & F is Cover of holds
ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) ; :: thesis: M is compact
now
let F be Subset-Family of ; :: thesis: ( F is Cover of & F is open implies ex GG being Subset-Family of st
( GG c= F & GG is Cover of & GG is finite ) )
set Z = { (Ball p,r) where p is Point of , r is Real : ex P being Subset of st
( P in F & Ball p,r c= P ) } ;
{ (Ball p,r) where p is Point of , r is Real : ex P being Subset of st
( P in F & Ball p,r c= P ) } c= bool the carrier of M
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (Ball p,r) where p is Point of , r is Real : ex P being Subset of st
( P in F & Ball p,r c= P ) } or a in bool the carrier of M )
assume a in { (Ball p,r) where p is Point of , r is Real : ex P being Subset of st
( P in F & Ball p,r c= P ) } ; :: thesis: a in bool the carrier of M
then ex p being Point of ex r being Real st
( a = Ball p,r & ex P being Subset of st
( P in F & Ball p,r c= P ) ) ;
hence a in bool the carrier of M ; :: thesis: verum
end;
then reconsider Z = { (Ball p,r) where p is Point of , r is Real : ex P being Subset of st
( P in F & Ball p,r c= P ) } as Subset-Family of ;
assume that
A9: F is Cover of and
A10: F is open ; :: thesis: ex GG being Subset-Family of st
( GG c= F & GG is Cover of & GG is finite )
the carrier of M c= union Z
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of M or a in union Z )
assume a in the carrier of M ; :: thesis: a in union Z
then reconsider p = a as Point of ;
( the carrier of (TopSpaceMetr M) c= union F & the carrier of (TopSpaceMetr M) = the carrier of M ) by A9, Th16, SETFAM_1:def 12;
then p in union F by TARSKI:def 3;
then consider P being set such that
A11: p in P and
A12: P in F by TARSKI:def 4;
reconsider P = P as Subset of by A12;
P is open by A10, A12, TOPS_2:def 1;
then consider r being real number such that
A13: r > 0 and
A14: Ball p,r c= P by A11, Th22;
reconsider r' = r as Element of REAL by XREAL_0:def 1;
A15: a in Ball p,r by A13, TBSP_1:16;
Ball p,r' in Z by A12, A14;
hence a in union Z by A15, TARSKI:def 4; :: thesis: verum
end;
then A16: Z is Cover of by SETFAM_1:def 12;
reconsider F' = F as non empty Subset-Family of by A9, TOPS_2:5;
defpred S1[ set , set ] means $1 c= $2;
Z is being_ball-family
proof
let P be set ; :: according to TOPMETR:def 4 :: thesis: ( P in Z implies ex p being Point of ex r being Real st P = Ball p,r )
assume P in Z ; :: thesis: ex p being Point of ex r being Real st P = Ball p,r
then ex p being Point of ex r being Real st
( P = Ball p,r & ex P being Subset of st
( P in F & Ball p,r c= P ) ) ;
hence ex p being Point of ex r being Real st P = Ball p,r ; :: thesis: verum
end;
then consider G being Subset-Family of such that
A17: G c= Z and
A18: G is Cover of and
A19: G is finite by A8, A16;
A20: for a being set st a in G holds
ex u being set st
( u in F' & S1[a,u] )
proof
let a be set ; :: thesis: ( a in G implies ex u being set st
( u in F' & S1[a,u] ) )
assume a in G ; :: thesis: ex u being set st
( u in F' & S1[a,u] )
then a in Z by A17;
then consider p being Point of , r being Real such that
A21: Ball p,r = a and
A22: ex P being Subset of st
( P in F & Ball p,r c= P ) ;
consider P being Subset of such that
A23: ( P in F & Ball p,r c= P ) by A22;
take P ; :: thesis: ( P in F' & S1[a,P] )
thus ( P in F' & S1[a,P] ) by A21, A23; :: thesis: verum
end;
consider f being Function of G,F' such that
A24: for a being set st a in G holds
S1[a,f . a] from FUNCT_2:sch 1(A20);
reconsider GG = rng f as Subset-Family of by TOPS_2:3;
take GG = GG; :: thesis: ( GG c= F & GG is Cover of & GG is finite )
thus GG c= F ; :: thesis: ( GG is Cover of & GG is finite )
the carrier of (TopSpaceMetr M) c= union GG
proof
A25: ( the carrier of (TopSpaceMetr M) = the carrier of M & the carrier of M c= union G ) by A18, Th16, SETFAM_1:def 12;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (TopSpaceMetr M) or a in union GG )
assume a in the carrier of (TopSpaceMetr M) ; :: thesis: a in union GG
then consider P being set such that
A26: a in P and
A27: P in G by A25, TARSKI:def 4;
A28: P c= f . P by A24, A27;
dom f = G by FUNCT_2:def 1;
then f . P in GG by A27, FUNCT_1:def 5;
hence a in union GG by A26, A28, TARSKI:def 4; :: thesis: verum
end;
hence GG is Cover of by SETFAM_1:def 12; :: thesis: GG is finite
dom f = G by FUNCT_2:def 1;
hence GG is finite by A19, FINSET_1:26; :: thesis: verum
end;
then TopSpaceMetr M is compact by COMPTS_1:def 3;
hence M is compact by Def6; :: thesis: verum
end;