let M be non empty MetrSpace; ( M is sequentially_compact implies TopSpaceMetr M is countably_compact )
assume A1:
M is sequentially_compact
; TopSpaceMetr M is countably_compact
A2:
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}
proof
let X be
Subset of
M;
( X is infinite implies ex x being Element of M st
for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
assume A3:
X is
infinite
;
ex x being Element of M st
for r being Real st 0 < r holds
Ball (x,r) meets X \ {x}
then consider S1 being
sequence of
X such that A4:
S1 is
one-to-one
by DICKSON:3;
A5:
rng S1 c= X
;
rng S1 c= [#] M
by XBOOLE_1:1;
then
S1 is
Function of
(dom S1),
([#] M)
by FUNCT_2:2;
then reconsider S1 =
S1 as
sequence of
([#] M) by A3, FUNCT_2:def 1;
rng S1 c= [#] M
;
then consider S2 being
sequence of
M such that A6:
( ex
N being
increasing sequence of
NAT st
S2 = S1 * N &
S2 is
convergent &
lim S2 in [#] M )
by A1, Def1;
set x =
lim S2;
rng S2 c= rng S1
by A6, RELAT_1:26;
then A7:
rng S2 c= X
by A5, XBOOLE_1:1;
take
lim S2
;
for r being Real st 0 < r holds
Ball ((lim S2),r) meets X \ {(lim S2)}
thus
for
r being
Real st
0 < r holds
Ball (
(lim S2),
r)
meets X \ {(lim S2)}
verumproof
let r be
Real;
( 0 < r implies Ball ((lim S2),r) meets X \ {(lim S2)} )
assume
0 < r
;
Ball ((lim S2),r) meets X \ {(lim S2)}
then consider n being
Nat such that A8:
for
m being
Nat st
m >= n holds
dist (
(S2 . m),
(lim S2))
< r
by A6, TBSP_1:def 3;
per cases
( S2 . n <> lim S2 or S2 . n = lim S2 )
;
suppose A11:
S2 . n = lim S2
;
Ball ((lim S2),r) meets X \ {(lim S2)}consider N being
increasing sequence of
NAT such that A12:
S2 = S1 * N
by A6;
for
x1,
x2 being
object st
x1 in NAT &
x2 in NAT &
N . x1 = N . x2 holds
x1 = x2
then
N is
one-to-one
by FUNCT_2:19;
then A16:
S2 is
one-to-one
by A4, A12, FUNCT_1:24;
A17:
n < n + 1
by NAT_1:16;
(
n in NAT &
n + 1
in NAT )
by ORDINAL1:def 12;
then
S2 . (n + 1) <> lim S2
by A11, A16, A17, FUNCT_2:19;
then A18:
not
S2 . (n + 1) in {(lim S2)}
by TARSKI:def 1;
S2 . (n + 1) in rng S2
by FUNCT_2:112;
then A19:
S2 . (n + 1) in X \ {(lim S2)}
by A7, A18, XBOOLE_0:def 5;
dist (
(S2 . (n + 1)),
(lim S2))
< r
by A8, A17;
then
S2 . (n + 1) in Ball (
(lim S2),
r)
by METRIC_1:11;
hence
Ball (
(lim S2),
r)
meets X \ {(lim S2)}
by A19, XBOOLE_0:def 4;
verum end; end;
end;
end;
A20:
for A being Subset of (TopSpaceMetr M) st A is infinite holds
not Der A is empty
TopSpaceMetr M is T_2
by PCOMPS_1:34;
hence
TopSpaceMetr M is countably_compact
by A20, COMPL_SP:28; verum