let M be non empty MetrSpace; ( 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:8, TBSP_1:9; ( M is totally_bounded & M is complete implies TopSpaceMetr M is compact )
assume that
A1:
M is totally_bounded
and
A2:
M is complete
; TopSpaceMetr M is compact
now for A being Subset of (TopSpaceMetr M) st A is infinite holds
not Der A is empty reconsider NULL =
0 as
Real ;
deffunc H1(
Nat)
-> set = 1
/ (1 + $1);
set cM = the
carrier of
M;
defpred S1[
object ,
object ]
means for
a,
b being
Subset of
M st $1
= a & $2
= b holds
(
b c= a &
diameter b <= (diameter a) / 2 );
defpred S2[
object ]
means for
a being
Subset of
M st
a = $1 holds
(
a is
bounded &
a is
infinite &
a is
closed );
consider seq being
Real_Sequence such that A3:
for
n being
Nat holds
seq . n = H1(
n)
from SEQ_1:sch 1();
set Ns =
NULL (#) seq;
A4:
for
x being
object st
x in bool the
carrier of
M &
S2[
x] holds
ex
y being
object st
(
y in bool the
carrier of
M &
S1[
x,
y] &
S2[
y] )
proof
let x be
object ;
( x in bool the carrier of M & S2[x] implies ex y being object st
( y in bool the carrier of M & S1[x,y] & S2[y] ) )
assume that A5:
x in bool the
carrier of
M
and A6:
S2[
x]
;
ex y being object st
( y in bool the carrier of M & S1[x,y] & S2[y] )
reconsider X =
x as
Subset of
M by A5;
reconsider X9 =
X as
Subset of
(TopSpaceMetr M) ;
set d =
diameter X;
per cases
( diameter X = 0 or diameter X > 0 )
by A6, TBSP_1:21;
suppose A8:
diameter X > 0
;
ex y being object st
( y in bool the carrier of M & S1[x,y] & S2[y] )then
(diameter X) / 4
> 0
by XREAL_1:224;
then consider F being
Subset-Family of
M such that A9:
F is
finite
and A10:
the
carrier of
M = union F
and A11:
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;
X is
infinite
by A6;
then consider Y being
Subset of
M such that A12:
Y in F
and A13:
Y /\ X is
infinite
by A9, A10, Th35;
set YX =
Y /\ X;
A14:
ex
w being
Point of
M st
Y = Ball (
w,
((diameter X) / 4))
by A11, A12;
then A15:
Y is
bounded
;
then A16:
diameter (Y /\ X) <= diameter Y
by TBSP_1:24, XBOOLE_1:17;
diameter Y <= 2
* ((diameter X) / 4)
by A8, A14, TBSP_1:23, XREAL_1:224;
then A17:
diameter (Y /\ X) <= (diameter X) / 2
by A16, XXREAL_0:2;
reconsider yx =
Y /\ X as
Subset of
(TopSpaceMetr M) ;
reconsider CYX =
Cl yx as
Subset of
M ;
take
CYX
;
( CYX in bool the carrier of M & S1[x,CYX] & S2[CYX] )A18:
yx c= Cl yx
by PRE_TOPC:18;
A19:
yx c= X9
by XBOOLE_1:17;
X is
closed
by A6;
then A20:
X9 is
closed
by Th6;
Y /\ X is
bounded
by A15, TBSP_1:14, XBOOLE_1:17;
hence
(
CYX in bool the
carrier of
M &
S1[
x,
CYX] &
S2[
CYX] )
by A13, A17, A18, A20, A19, Th6, Th8, TOPS_1:5;
verum end;
end; consider G being
Subset-Family of
M such that A21:
G is
finite
and A22:
the
carrier of
M = union G
and A23:
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;
let A be
Subset of
(TopSpaceMetr M);
( A is infinite implies not Der A is empty )assume
A is
infinite
;
not Der A is empty then consider X being
Subset of
M such that A24:
X in G
and A25:
X /\ A is
infinite
by A21, A22, Th35;
reconsider XA =
X /\ A as
Subset of
M ;
reconsider xa =
XA as
Subset of
(TopSpaceMetr M) ;
reconsider CXA =
Cl xa as
Subset of
M ;
A26:
(
XA is
bounded &
diameter XA <= 1 )
then
CXA is
bounded
by Th8;
then A30:
0 <= diameter CXA
by TBSP_1:21;
xa c= Cl xa
by PRE_TOPC:18;
then A31:
(
CXA in bool the
carrier of
M &
S2[
CXA] )
by A25, A26, Th6, Th8;
consider f being
Function such that A32:
(
dom f = NAT &
rng f c= bool the
carrier of
M )
and A33:
f . 0 = CXA
and A34:
for
k being
Nat holds
(
S1[
f . k,
f . (k + 1)] &
S2[
f . k] )
from TREES_2:sch 5(A31, A4);
reconsider f =
f as
SetSequence of
M by A32, FUNCT_2:2;
A35:
for
n being
Nat holds
f . n is
bounded
by A34;
for
n being
Nat holds
f . n is
closed
by A34;
then reconsider f =
f as
non-empty pointwise_bounded closed SetSequence of
M by A36, A35, Def1, Def8, FUNCT_1:def 9;
A37:
(NULL (#) seq) . 0 = NULL * (seq . 0)
by SEQ_1:9;
for
n being
Nat holds
f . (n + 1) c= f . n
by A34;
then A38:
f is
non-ascending
by KURATO_0:def 3;
set df =
diameter f;
defpred S3[
Nat]
means (
(NULL (#) seq) . $1
<= (diameter f) . $1 &
(diameter f) . $1
<= seq . $1 );
A39:
for
n being
Nat st
S3[
n] holds
S3[
n + 1]
A46:
seq . 0 = 1
/ (1 + 0)
by A3;
A47:
for
n being
Nat holds
seq . n = 1
/ (n + 1)
by A3;
then A48:
seq is
convergent
by SEQ_4:31;
diameter CXA <= 1
by A26, Th8;
then A49:
S3[
0 ]
by A33, A30, A46, A37, Def2;
A50:
for
n being
Nat holds
S3[
n]
from NAT_1:sch 2(A49, A39);
A51:
NULL (#) seq is
convergent
by A47, SEQ_2:7, SEQ_4:31;
A52:
lim seq = 0
by A47, SEQ_4:31;
then A53:
lim (NULL (#) seq) = NULL * 0
by A47, SEQ_2:8, SEQ_4:31;
then A54:
lim (diameter f) = 0
by A48, A52, A51, A50, SEQ_2:20;
then
not
meet f is
empty
by A2, A38, Th10;
then consider p being
object such that A55:
p in meet f
by XBOOLE_0:def 1;
reconsider p =
p as
Point of
(TopSpaceMetr M) by A55;
reconsider p9 =
p as
Point of
M ;
A56:
diameter f is
convergent
by A48, A52, A51, A53, A50, SEQ_2:19;
now for U being open Subset of (TopSpaceMetr M) st p in U holds
ex s9 being Point of (TopSpaceMetr M) st
( s9 in A /\ U & s9 <> p )let U be
open Subset of
(TopSpaceMetr M);
( p in U implies ex s9 being Point of (TopSpaceMetr M) st
( s9 in A /\ U & s9 <> p ) )assume
p in U
;
ex s9 being Point of (TopSpaceMetr M) st
( s9 in A /\ U & s9 <> p )then consider r being
Real such that A57:
r > 0
and A58:
Ball (
p9,
r)
c= U
by TOPMETR:15;
r / 2
> 0
by A57, XREAL_1:215;
then consider n being
Nat such that A59:
for
m being
Nat st
n <= m holds
|.(((diameter f) . m) - 0).| < r / 2
by A54, A56, SEQ_2:def 7;
p in f . n
by A55, KURATO_0:3;
then A60:
{p} c= f . n
by ZFMISC_1:31;
f . n is
infinite
by A34;
then
{p} c< f . n
by A60, XBOOLE_0:def 8;
then
(f . n) \ {p} <> {}
by XBOOLE_1:105;
then consider q being
object such that A61:
q in (f . n) \ {p}
by XBOOLE_0:def 1;
reconsider q =
q as
Point of
(TopSpaceMetr M) by A61;
A62:
q in f . n
by A61, ZFMISC_1:56;
A63:
q in f . n
by A61, ZFMISC_1:56;
reconsider q9 =
q as
Point of
M ;
q <> p
by A61, ZFMISC_1:56;
then A64:
dist (
p9,
q9)
<> 0
by METRIC_1:2;
reconsider B =
Ball (
q9,
(dist (p9,q9))) as
Subset of
(TopSpaceMetr M) ;
A65:
dist (
p9,
q9)
>= 0
by METRIC_1:5;
dist (
q9,
q9)
= 0
by METRIC_1:1;
then A66:
q in B
by A64, A65, METRIC_1:11;
Ball (
q9,
(dist (p9,q9)))
in Family_open_set M
by PCOMPS_1:29;
then A67:
B is
open
by PRE_TOPC:def 2;
f . n c= Cl xa
by A33, A38, PROB_1:def 4;
then
B meets xa
by A67, A66, A62, PRE_TOPC:24;
then consider s being
object such that A68:
s in B
and A69:
s in xa
by XBOOLE_0:3;
reconsider s =
s as
Point of
M by A68;
reconsider s9 =
s as
Point of
(TopSpaceMetr M) ;
take s9 =
s9;
( s9 in A /\ U & s9 <> p )A70:
(NULL (#) seq) . n = NULL * (seq . n)
by SEQ_1:9;
A71:
|.(((diameter f) . n) - 0).| < r / 2
by A59;
A72:
f . n is
bounded
by A34;
(diameter f) . n >= (NULL (#) seq) . n
by A50;
then
(diameter f) . n < r / 2
by A70, A71, ABSVALUE:def 1;
then A73:
diameter (f . n) < r / 2
by Def2;
p in f . n
by A55, KURATO_0:3;
then
dist (
p9,
q9)
<= diameter (f . n)
by A63, A72, TBSP_1:def 8;
then A74:
dist (
p9,
q9)
< r / 2
by A73, XXREAL_0:2;
dist (
q9,
s)
< dist (
p9,
q9)
by A68, METRIC_1:11;
then
dist (
q9,
s)
< r / 2
by A74, XXREAL_0:2;
then A75:
(dist (p9,q9)) + (dist (q9,s)) < (r / 2) + (r / 2)
by A74, XREAL_1:8;
dist (
p9,
s)
<= (dist (p9,q9)) + (dist (q9,s))
by METRIC_1:4;
then
dist (
p9,
s)
< r
by A75, XXREAL_0:2;
then A76:
s in Ball (
p9,
r)
by METRIC_1:11;
s in A
by A69, XBOOLE_0:def 4;
hence
(
s9 in A /\ U &
s9 <> p )
by A58, A68, A76, METRIC_1:11, XBOOLE_0:def 4;
verum end; hence
not
Der A is
empty
by TOPGEN_1:17;
verum end;
then
TopSpaceMetr M is countably_compact
by Th27;
hence
TopSpaceMetr M is compact
by Th34; verum