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 )
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: verumproof
assume A7:
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
set TM =
TopSpaceMetr M;
now 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 ) )assume that A8:
F is
Cover of
(TopSpaceMetr M)
and A9:
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 )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 ;
A10:
Z is
being_ball-family
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
M ;
( the
carrier of
(TopSpaceMetr M) c= union F & the
carrier of
(TopSpaceMetr M) = the
carrier of
M )
by A8, Th1, Th16;
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 A9, A12, TOPS_2:def 1;
then consider r being
real number such that A13:
(
r > 0 &
Ball p,
r c= P )
by A11, Th22;
reconsider r' =
r as
Element of
REAL by XREAL_0:def 1;
A14:
a in Ball p,
r
by A13, TBSP_1:16;
Ball p,
r' in Z
by A12, A13;
hence
a in union Z
by A14, TARSKI:def 4;
:: thesis: verum
end; then
Z is
Cover of
M
by SETFAM_1:def 12;
then consider G being
Subset-Family of
M such that A15:
G c= Z
and A16:
G is
Cover of
M
and A17:
G is
finite
by A7, A10;
reconsider F' =
F as non
empty Subset-Family of
(TopSpaceMetr M) by A8, TOPS_2:5;
defpred S1[
set ,
set ]
means $1
c= $2;
A18:
for
a being
set st
a in G holds
ex
u being
set st
(
u in F' &
S1[
a,
u] )
consider f being
Function of
G,
F' such that A22:
for
a being
set st
a in G holds
S1[
a,
f . a]
from FUNCT_2:sch 1(A18);
reconsider GG =
rng f as
Subset-Family of
(TopSpaceMetr M) by TOPS_2:3;
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
hence
GG is
Cover of
(TopSpaceMetr M)
by Th1;
:: thesis: GG is finite
dom f = G
by FUNCT_2:def 1;
hence
GG is
finite
by A17, 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;