let M be non empty MetrSpace; ( 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 ) )
( ( 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 )
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 )
verumproof
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 )
;
M is compact
now let F be
Subset-Family of
(TopSpaceMetr M);
( 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
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
;
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
set ;
TARSKI:def 3 ( not a in the carrier of M or a in union Z )
assume
a in the
carrier of
M
;
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 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
(TopSpaceMetr M) 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 r9 =
r as
Element of
REAL by XREAL_0:def 1;
A15:
a in Ball p,
r
by A13, TBSP_1:16;
Ball p,
r9 in Z
by A12, A14;
hence
a in union Z
by A15, TARSKI:def 4;
verum
end; then A16:
Z is
Cover of
M
by SETFAM_1:def 12;
reconsider F9 =
F as non
empty Subset-Family of
(TopSpaceMetr M) by A9, TOPS_2:5;
defpred S1[
set ,
set ]
means $1
c= $2;
Z is
being_ball-family
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
set st
a in G holds
ex
u being
set st
(
u in F9 &
S1[
a,
u] )
consider f being
Function of
G,
F9 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
(TopSpaceMetr M) by TOPS_2:3;
take GG =
GG;
( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )thus
GG c= F
;
( GG is Cover of (TopSpaceMetr M) & GG is finite )
the
carrier of
(TopSpaceMetr M) c= union GG
hence
GG is
Cover of
(TopSpaceMetr M)
by SETFAM_1:def 12;
GG is finite
dom f = G
by FUNCT_2:def 1;
hence
GG is
finite
by A19, FINSET_1:26;
verum end;
then
TopSpaceMetr M is
compact
by COMPTS_1:def 3;
hence
M is
compact
by Def6;
verum
end;