let M be non empty MetrSpace; :: thesis: ( M is compact iff for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) )
thus ( M is compact implies for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ) :: thesis: ( ( for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ) implies M is compact )

proof

set TM = TopSpaceMetr M;
assume M is compact ; :: thesis: for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite )
then A1: TopSpaceMetr M is compact ;
let F be Subset-Family of M; :: thesis: ( F is being_ball-family & F is Cover of M implies ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) )
reconsider TF = F as Subset-Family of (TopSpaceMetr M) ;
assume that
A2: F is being_ball-family and
A3: F is Cover of M ; :: thesis: ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite )
A4: TF is open

proof

let P be Subset of (TopSpaceMetr M); :: according to TOPS_2:def 1 :: thesis: ( not P in TF or P is open )
reconsider P9 = P as Subset of M ;
assume P in TF ; :: thesis: P is open
then ex p being Point of M ex r being Real st P9 = Ball (p,r) by A2;
hence P is open by Th14; :: thesis: verum

end;

the carrier of M c= union F by A3, SETFAM_1:def 11;
then the carrier of (TopSpaceMetr M) c= union TF ;
then TF is Cover of (TopSpaceMetr M) by SETFAM_1:def 11;
then consider TG being Subset-Family of (TopSpaceMetr M) such that
A5: TG c= TF and
A6: TG is Cover of (TopSpaceMetr M) and
A7: TG is finite by A1, A4, COMPTS_1:def 1;
reconsider G = TG as Subset-Family of M ;
take G ; :: thesis: ( G c= F & G is Cover of M & G is finite )
the carrier of (TopSpaceMetr M) c= union TG by A6, SETFAM_1:def 11;
then the carrier of M c= union G ;
hence ( G c= F & G is Cover of M & G is finite ) by A5, A7, SETFAM_1:def 11; :: thesis: verum

end;

thus ( ( for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ) implies M is compact ) :: thesis: verum

proof

set TM = TopSpaceMetr M;
assume A8: for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ; :: thesis: M is compact

now :: thesis: for F being Subset-Family of (TopSpaceMetr M) st F is Cover of (TopSpaceMetr M) & F is open holds
ex GG being Subset-Family of (TopSpaceMetr M) st
( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )

let F be Subset-Family of (TopSpaceMetr M); :: thesis: ( F is Cover of (TopSpaceMetr M) & F is open implies ex GG being Subset-Family of (TopSpaceMetr M) st
( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite ) )
set Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } ;
{ (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } c= bool the carrier of M

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) 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 M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } ; :: thesis: a in bool the carrier of M
then ex p being Point of M ex r being Real st
( a = Ball (p,r) & ex P being Subset of (TopSpaceMetr M) 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 M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } as Subset-Family of M ;
assume that
A9: F is Cover of (TopSpaceMetr M) and
A10: F is open ; :: thesis: ex GG being Subset-Family of (TopSpaceMetr M) st
( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )
the carrier of M c= union Z

proof

let a be object ; :: 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 M ;
( the carrier of (TopSpaceMetr M) c= union F & the carrier of (TopSpaceMetr M) = the carrier of M ) by A9, SETFAM_1:def 11;
then p in union F ;
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 (TopSpaceMetr M) by A12;
P is open by A10, A12;
then consider r being Real such that
A13: r > 0 and
A14: Ball (p,r) c= P by A11, Th15;
reconsider r9 = r as Element of REAL by XREAL_0:def 1;
A15: a in Ball (p,r) by A13, TBSP_1:11;
Ball (p,r9) in Z by A12, A14;
hence a in union Z by A15, TARSKI:def 4; :: thesis: verum

end;

then A16: Z is Cover of M by SETFAM_1:def 11;
reconsider F9 = F as non empty Subset-Family of (TopSpaceMetr M) by A9, TOPS_2:3;
defpred S₁[ object , object ] means ex D1, D2 being set st
( D1 = $1 & D2 = $2 & D1 c= D2 );
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 M ex r being Real st P = Ball (p,r) )
assume P in Z ; :: thesis: ex p being Point of M ex r being Real st P = Ball (p,r)
then ex p being Point of M ex r being Real st
( P = Ball (p,r) & ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) ) ;
hence ex p being Point of M ex r being Real st P = Ball (p,r) ; :: thesis: verum

end;

then consider G being Subset-Family of M such that
A17: G c= Z and
A18: G is Cover of M and
A19: G is finite by A8, A16;
A20: for a being object st a in G holds
ex u being object st
( u in F9 & S₁[a,u] )

proof

let a be object ; :: thesis: ( a in G implies ex u being object st
( u in F9 & S₁[a,u] ) )
assume a in G ; :: thesis: ex u being object st
( u in F9 & S₁[a,u] )
then a in Z by A17;
then consider p being Point of M, r being Real such that
A21: Ball (p,r) = a and
A22: ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) ;
consider P being Subset of (TopSpaceMetr M) such that
A23: ( P in F & Ball (p,r) c= P ) by A22;
take P ; :: thesis: ( P in F9 & S₁[a,P] )
thus ( P in F9 & S₁[a,P] ) by A21, A23; :: thesis: verum

end;

consider f being Function of G,F9 such that
A24: for a being object st a in G holds
S₁[a,f . a] from FUNCT_2:sch 1(A20);
reconsider GG = rng f as Subset-Family of (TopSpaceMetr M) by TOPS_2:2;
take GG = GG; :: thesis: ( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )
thus GG c= F ; :: thesis: ( GG is Cover of (TopSpaceMetr M) & 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, SETFAM_1:def 11;
let a be object ; :: 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;
S₁[P,f . P] by A24, A27;
then A28: P c= f . P ;
dom f = G by FUNCT_2:def 1;
then f . P in GG by A27, FUNCT_1:def 3;
hence a in union GG by A26, A28, TARSKI:def 4; :: thesis: verum

end;

hence GG is Cover of (TopSpaceMetr M) by SETFAM_1:def 11; :: thesis: GG is finite
dom f = G by FUNCT_2:def 1;
hence GG is finite by A19, FINSET_1:8; :: thesis: verum

end;

then TopSpaceMetr M is compact by COMPTS_1:def 1;
hence M is compact ; :: thesis: verum

end;