let M be non empty MetrSpace; ( TopSpaceMetr M is countably_compact implies M is sequentially_compact )
assume A1:
TopSpaceMetr M is countably_compact
; M is sequentially_compact
A2:
TopSpaceMetr M is T_2
by PCOMPS_1:34;
A3:
for X being Subset of M st X is infinite holds
ex x being Element of M st
for r being Real st 0 < r holds
Ball (x,r) meets X \ {x}
for x being sequence of M st rng x c= [#] M holds
ex xN being sequence of M st
( ex N being increasing sequence of NAT st xN = x * N & xN is convergent & lim xN in [#] M )
proof
let x be
sequence of
M;
( rng x c= [#] M implies ex xN being sequence of M st
( ex N being increasing sequence of NAT st xN = x * N & xN is convergent & lim xN in [#] M ) )
assume
rng x c= [#] M
;
ex xN being sequence of M st
( ex N being increasing sequence of NAT st xN = x * N & xN is convergent & lim xN in [#] M )
per cases
( rng x is finite or rng x is infinite )
;
suppose
rng x is
infinite
;
ex xN being sequence of M st
( ex N being increasing sequence of NAT st xN = x * N & xN is convergent & lim xN in [#] M )then consider z being
Element of
M such that A12:
for
r being
Real st
0 < r holds
Ball (
z,
r)
meets (rng x) \ {z}
by A3;
Ball (
z,1)
meets (rng x) \ {z}
by A12;
then consider w being
object such that A13:
w in (Ball (z,1)) /\ ((rng x) \ {z})
by XBOOLE_0:def 1;
reconsider w =
w as
Point of
M by A13;
w in (rng x) \ {z}
by A13, XBOOLE_0:def 4;
then
w in rng x
by XBOOLE_0:def 5;
then consider N0 being
Element of
NAT such that A14:
w = x . N0
by FUNCT_2:113;
defpred S1[
Nat,
Nat,
Nat]
means ( $2
< $3 &
x . $3
in Ball (
z,
(1 / (2 + $1))) );
A15:
for
n being
Nat for
ix being
Element of
NAT ex
iy being
Element of
NAT st
S1[
n,
ix,
iy]
proof
let n be
Nat;
for ix being Element of NAT ex iy being Element of NAT st S1[n,ix,iy]let ix be
Element of
NAT ;
ex iy being Element of NAT st S1[n,ix,iy]
assume A16:
for
iy being
Element of
NAT holds not
S1[
n,
ix,
iy]
;
contradiction
A17:
(Ball (z,(1 / (2 + n)))) /\ ((rng x) \ {z}) c= Ball (
z,
(1 / (2 + n)))
by XBOOLE_1:17;
for
g being
object st
g in (Ball (z,(1 / (2 + n)))) /\ ((rng x) \ {z}) holds
g in x .: (Segm (ix + 1))
then
(Ball (z,(1 / (2 + n)))) /\ ((rng x) \ {z}) c= x .: (Segm (ix + 1))
by TARSKI:def 3;
hence
contradiction
by A12, LM3;
verum
end; consider N being
sequence of
NAT such that A20:
(
N . 0 = N0 & ( for
n being
Nat holds
S1[
n,
N . n,
N . (n + 1)] ) )
from RECDEF_1:sch 2(A15);
N is
increasing
by A20;
then reconsider N =
N as
increasing sequence of
NAT ;
defpred S2[
Nat]
means x . (N . $1) in Ball (
z,
(1 / (1 + $1)));
A21:
S2[
0 ]
by A13, A14, A20, XBOOLE_0:def 4;
A22:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume
S2[
k]
;
S2[k + 1]
(
N . k < N . (k + 1) &
x . (N . (k + 1)) in Ball (
z,
(1 / (2 + k))) )
by A20;
hence
S2[
k + 1]
;
verum
end; A23:
for
i being
Nat holds
S2[
i]
from NAT_1:sch 2(A21, A22);
now for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
dist (((x * N) . m),z) < rlet r be
Real;
( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
dist (((x * N) . m),z) < r )assume A24:
0 < r
;
ex n being Nat st
for m being Nat st n <= m holds
dist (((x * N) . m),z) < rconsider n being
Nat such that A25:
r " < n
by SEQ_4:3;
A26:
1
/ n < 1
/ (r ")
by A24, A25, XREAL_1:76;
A27:
0 < n
by A24, A25;
take n =
n;
for m being Nat st n <= m holds
dist (((x * N) . m),z) < rthus
for
m being
Nat st
n <= m holds
dist (
((x * N) . m),
z)
< r
verumproof
let m be
Nat;
( n <= m implies dist (((x * N) . m),z) < r )
assume
n <= m
;
dist (((x * N) . m),z) < r
then
n + 0 < m + 1
by XREAL_1:8;
then A28:
1
/ (1 + m) <= 1
/ n
by A27, XREAL_1:118;
x . (N . m) in Ball (
z,
(1 / (1 + m)))
by A23;
then A29:
dist (
(x . (N . m)),
z)
< 1
/ n
by A28, METRIC_1:11, XXREAL_0:2;
x . (N . m) = (x * N) . m
by FUNCT_2:15, ORDINAL1:def 12;
hence
dist (
((x * N) . m),
z)
< r
by A26, A29, XXREAL_0:2;
verum
end; end; then A30:
x * N is
convergent
;
lim (x * N) in [#] M
;
hence
ex
xN being
sequence of
M st
( ex
N being
increasing sequence of
NAT st
xN = x * N &
xN is
convergent &
lim xN in [#] M )
by A30;
verum end; end;
end;
then
[#] M is sequentially_compact
;
hence
M is sequentially_compact
; verum