let M be non empty MetrSpace; :: thesis: ( TopSpaceMetr M is compact iff ( M is totally_bounded & M is complete ) )
set T = TopSpaceMetr M;
thus
( TopSpaceMetr M is compact implies ( M is totally_bounded & M is complete ) )
by TBSP_1:10, TBSP_1:12; :: thesis: ( M is totally_bounded & M is complete implies TopSpaceMetr M is compact )
assume that
A1:
M is totally_bounded
and
A2:
M is complete
; :: thesis: TopSpaceMetr M is compact
now let A be
Subset of
(TopSpaceMetr M);
:: thesis: ( not A is finite implies not Der A is empty )assume A3:
not
A is
finite
;
:: thesis: not Der A is empty consider G being
Subset-Family of
M such that A4:
G is
finite
and A5:
the
carrier of
M = union G
and A6:
for
C being
Subset of
M st
C in G holds
ex
w being
Point of
M st
C = Ball w,
(1 / 2)
by A1, TBSP_1:def 1;
consider X being
Subset of
M such that A7:
(
X in G & not
X /\ A is
finite )
by A3, A4, A5, Th36;
defpred S1[
set ]
means for
a being
Subset of
M st
a = $1 holds
(
a is
bounded & not
a is
finite &
a is
closed );
defpred S2[
set ,
set ]
means for
a,
b being
Subset of
M st $1
= a & $2
= b holds
(
b c= a &
diameter b <= (diameter a) / 2 );
reconsider XA =
X /\ A as
Subset of
M ;
A8:
(
XA is
bounded &
diameter XA <= 1 )
reconsider xa =
XA as
Subset of
(TopSpaceMetr M) ;
reconsider CXA =
Cl xa as
Subset of
M ;
set cM = the
carrier of
M;
xa c= Cl xa
by PRE_TOPC:48;
then A10:
(
CXA in bool the
carrier of
M &
S1[
CXA] )
by A7, A8, Th6, Th8;
A11:
for
x being
set st
x in bool the
carrier of
M &
S1[
x] holds
ex
y being
set st
(
y in bool the
carrier of
M &
S2[
x,
y] &
S1[
y] )
proof
let x be
set ;
:: thesis: ( x in bool the carrier of M & S1[x] implies ex y being set st
( y in bool the carrier of M & S2[x,y] & S1[y] ) )
assume A12:
(
x in bool the
carrier of
M &
S1[
x] )
;
:: thesis: ex y being set st
( y in bool the carrier of M & S2[x,y] & S1[y] )
reconsider X =
x as
Subset of
M by A12;
reconsider X' =
X as
Subset of
(TopSpaceMetr M) ;
set d =
diameter X;
per cases
( diameter X = 0 or diameter X > 0 )
by A12, TBSP_1:29;
suppose
diameter X > 0
;
:: thesis: ex y being set st
( y in bool the carrier of M & S2[x,y] & S1[y] )then A15:
(diameter X) / 4
> 0
by XREAL_1:226;
then consider F being
Subset-Family of
M such that A16:
F is
finite
and A17:
the
carrier of
M = union F
and A18:
for
C being
Subset of
M st
C in F holds
ex
w being
Point of
M st
C = Ball w,
((diameter X) / 4)
by A1, TBSP_1:def 1;
not
X is
finite
by A12;
then consider Y being
Subset of
M such that A19:
(
Y in F & not
Y /\ X is
finite )
by A16, A17, Th36;
set YX =
Y /\ X;
consider w being
Point of
M such that A20:
Y = Ball w,
((diameter X) / 4)
by A18, A19;
(
Y is
bounded &
Y /\ X c= Y )
by A20, TBSP_1:19, XBOOLE_1:17;
then A21:
(
Y /\ X is
bounded &
diameter (Y /\ X) <= diameter Y &
diameter Y <= 2
* ((diameter X) / 4) )
by A15, A20, TBSP_1:21, TBSP_1:31, TBSP_1:32;
then A22:
diameter (Y /\ X) <= (diameter X) / 2
by XXREAL_0:2;
reconsider yx =
Y /\ X as
Subset of
(TopSpaceMetr M) ;
reconsider CYX =
Cl yx as
Subset of
M ;
take
CYX
;
:: thesis: ( CYX in bool the carrier of M & S2[x,CYX] & S1[CYX] )A23:
yx c= Cl yx
by PRE_TOPC:48;
X is
closed
by A12;
then
(
X' is
closed &
yx c= X' )
by Th6, XBOOLE_1:17;
hence
(
CYX in bool the
carrier of
M &
S2[
x,
CYX] &
S1[
CYX] )
by A19, A21, A22, A23, Th6, Th8, TOPS_1:31;
:: thesis: verum end;
end; consider f being
Function such that A24:
(
dom f = NAT &
rng f c= bool the
carrier of
M )
and A25:
f . 0 = CXA
and A26:
for
k being
Element of
NAT holds
(
S2[
f . k,
f . (k + 1)] &
S1[
f . k] )
from TREES_2:sch 5(A10, A11);
reconsider f =
f as
SetSequence of
M by A24, FUNCT_2:4;
then reconsider f =
f as
non-empty bounded closed SetSequence of
M by A27, A29, Def1, Def8, FUNCT_1:def 15;
for
n being
Element of
NAT holds
f . (n + 1) c= f . n
by A26;
then A30:
f is
non-ascending
by KURATO_2:def 5;
deffunc H1(
Element of
NAT )
-> Element of
REAL = 1
/ (1 + $1);
consider seq being
Real_Sequence such that A31:
for
n being
Element of
NAT holds
seq . n = H1(
n)
from SEQ_1:sch 1();
reconsider NULL =
0 as
Real ;
set Ns =
NULL (#) seq;
for
n being
Element of
NAT holds
seq . n = 1
/ (n + 1)
by A31;
then A32:
(
seq is
convergent &
lim seq = 0 )
by SEQ_4:45;
then A33:
(
NULL (#) seq is
convergent &
lim (NULL (#) seq) = NULL * 0 )
by SEQ_2:21, SEQ_2:22;
set df =
diameter f;
defpred S3[
Element of
NAT ]
means (
(NULL (#) seq) . $1
<= (diameter f) . $1 &
(diameter f) . $1
<= seq . $1 );
CXA is
bounded
by A8, Th8;
then
(
0 <= diameter CXA &
diameter CXA <= 1 &
seq . 0 = 1
/ (1 + 0 ) &
(NULL (#) seq) . 0 = NULL * (seq . 0 ) )
by A8, A31, Th8, SEQ_1:13, TBSP_1:29;
then A34:
S3[
0 ]
by A25, Def2;
A35:
for
n being
Element of
NAT st
S3[
n] holds
S3[
n + 1]
A39:
for
n being
Element of
NAT holds
S3[
n]
from NAT_1:sch 1(A34, A35);
then A40:
(
lim (diameter f) = 0 &
diameter f is
convergent )
by A32, A33, SEQ_2:33, SEQ_2:34;
then
not
meet f is
empty
by A2, A30, Th10;
then consider p being
set such that A41:
p in meet f
by XBOOLE_0:def 1;
reconsider p =
p as
Point of
(TopSpaceMetr M) by A41;
reconsider p' =
p as
Point of
M ;
now let U be
open Subset of
(TopSpaceMetr M);
:: thesis: ( p in U implies ex s' being Point of (TopSpaceMetr M) st
( s' in A /\ U & s' <> p ) )assume A42:
p in U
;
:: thesis: ex s' being Point of (TopSpaceMetr M) st
( s' in A /\ U & s' <> p )consider r being
real number such that A43:
(
r > 0 &
Ball p',
r c= U )
by A42, TOPMETR:22;
r / 2
> 0
by A43, XREAL_1:217;
then consider n being
Element of
NAT such that A44:
for
m being
Element of
NAT st
n <= m holds
abs (((diameter f) . m) - 0 ) < r / 2
by A40, SEQ_2:def 7;
not
f . n is
finite
by A26;
then
(
card {p} in card (f . n) &
p in f . n )
by A41, CARD_FIL:1, KURATO_2:6;
then
(
{p} <> f . n &
{p} c= f . n )
by ZFMISC_1:37;
then
{p} c< f . n
by XBOOLE_0:def 8;
then
(f . n) \ {p} <> {}
by XBOOLE_1:105;
then consider q being
set such that A45:
q in (f . n) \ {p}
by XBOOLE_0:def 1;
reconsider q =
q as
Point of
(TopSpaceMetr M) by A45;
reconsider q' =
q as
Point of
M ;
reconsider B =
Ball q',
(dist p',q') as
Subset of
(TopSpaceMetr M) ;
q <> p
by A45, ZFMISC_1:64;
then
(
Ball q',
(dist p',q') in Family_open_set M &
dist q',
q' = 0 &
dist p',
q' <> 0 &
dist p',
q' >= 0 )
by METRIC_1:1, METRIC_1:2, METRIC_1:5, PCOMPS_1:33;
then
(
B is
open &
q in B &
f . n c= Cl xa &
q in f . n )
by A25, A30, A45, METRIC_1:12, PRE_TOPC:def 5, PROB_1:def 6, ZFMISC_1:64;
then
B meets xa
by PRE_TOPC:54;
then consider s being
set such that A46:
(
s in B &
s in xa )
by XBOOLE_0:3;
reconsider s =
s as
Point of
M by A46;
reconsider s' =
s as
Point of
(TopSpaceMetr M) ;
take s' =
s';
:: thesis: ( s' in A /\ U & s' <> p )
(
(diameter f) . n >= (NULL (#) seq) . n &
(NULL (#) seq) . n = NULL * (seq . n) &
abs (((diameter f) . n) - 0 ) < r / 2 )
by A39, A44, SEQ_1:13;
then
(
(diameter f) . n < r / 2 &
p in f . n &
q in f . n &
f . n is
bounded )
by A26, A41, A45, ABSVALUE:def 1, KURATO_2:6, ZFMISC_1:64;
then
(
dist p',
q' <= diameter (f . n) &
diameter (f . n) < r / 2 )
by Def2, TBSP_1:def 10;
then A47:
(
dist p',
q' < r / 2 &
dist q',
s < dist p',
q' )
by A46, METRIC_1:12, XXREAL_0:2;
then
dist q',
s < r / 2
by XXREAL_0:2;
then
(
dist p',
s <= (dist p',q') + (dist q',s) &
(dist p',q') + (dist q',s) < (r / 2) + (r / 2) )
by A47, METRIC_1:4, XREAL_1:10;
then
dist p',
s < r
by XXREAL_0:2;
then
s in Ball p',
r
by METRIC_1:12;
then
(
s in U &
s in A )
by A43, A46, XBOOLE_0:def 4;
hence
(
s' in A /\ U &
s' <> p )
by A46, METRIC_1:12, XBOOLE_0:def 4;
:: thesis: verum end; hence
not
Der A is
empty
by TOPGEN_1:19;
:: thesis: verum end;
then
TopSpaceMetr M is countably_compact
by Th28;
hence
TopSpaceMetr M is compact
by Th35; :: thesis: verum