let M be non empty MetrSpace; :: thesis: ( M is sequentially_compact implies TopSpaceMetr M is countably_compact )
assume A1: M is sequentially_compact ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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)} :: thesis: verum
proof
let r be Real; :: thesis: ( 0 < r implies Ball ((lim S2),r) meets X \ {(lim S2)} )
assume 0 < r ; :: thesis: 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 ; :: thesis: 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
proof
let x1, x2 be object ; :: thesis: ( x1 in NAT & x2 in NAT & N . x1 = N . x2 implies x1 = x2 )
assume A13: ( x1 in NAT & x2 in NAT ) ; :: thesis: ( not N . x1 = N . x2 or x1 = x2 )
then reconsider n = x1, m = x2 as Nat ;
assume A14: N . x1 = N . x2 ; :: thesis: x1 = x2
assume x1 <> x2 ; :: thesis: contradiction
then A15: ( n < m or m < n ) by XXREAL_0:1;
dom N = NAT by FUNCT_2:def 1;
hence contradiction by A13, A14, A15, SEQM_3:def 1; :: thesis: verum
end;
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; :: thesis: verum
end;
end;
end;
end;
A20: for A being Subset of (TopSpaceMetr M) st A is infinite holds
not Der A is empty
proof
let A be Subset of (TopSpaceMetr M); :: thesis: ( A is infinite implies not Der A is empty )
assume A21: A is infinite ; :: thesis: not Der A is empty
reconsider X = A as Subset of M ;
consider x being Element of M such that
A22: for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} by A2, A21;
reconsider y = x as Point of (TopSpaceMetr M) ;
y is_an_accumulation_point_of A by A22, Th7;
hence not Der A is empty by TOPGEN_1:16; :: thesis: verum
end;
TopSpaceMetr M is T_2 by PCOMPS_1:34;
hence TopSpaceMetr M is countably_compact by A20, COMPL_SP:28; :: thesis: verum