let M be non empty MetrSpace; :: thesis: ( TopSpaceMetr M is countably_compact implies M is sequentially_compact )
assume A1: TopSpaceMetr M is countably_compact ; :: thesis: 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}
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 A4: 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}
reconsider A = X as Subset of (TopSpaceMetr M) ;
not Der A is empty by A1, A2, A4, COMPL_SP:28;
then consider z being object such that
A5: z in Der A ;
A6: z is_an_accumulation_point_of A by A5, TOPGEN_1:16;
reconsider z = z as Point of (TopSpaceMetr M) by A5;
reconsider x = z as Element of M ;
take x ; :: thesis: for r being Real st 0 < r holds
Ball (x,r) meets X \ {x}
thus for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} by A6, Th7; :: thesis: verum
end;
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; :: thesis: ( 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 ; :: thesis: 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 finite ; :: thesis: 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 the carrier of M such that
A7: ( x " {z} c= NAT & x " {z} is infinite ) by LM1;
consider N being increasing sequence of NAT such that
A8: rng N c= x " {z} by A7, LM2;
set xN = x * N;
take x * N ; :: thesis: ( ex N being increasing sequence of NAT st x * N = x * N & x * N is convergent & lim (x * N) in [#] M )
A9: for n being Nat holds (x * N) . n = z
proof
let n be Nat; :: thesis: (x * N) . n = z
N . n in rng N by FUNCT_2:4, ORDINAL1:def 12;
then x . (N . n) in {z} by A8, FUNCT_2:38;
then x . (N . n) = z by TARSKI:def 1;
hence (x * N) . n = z by FUNCT_2:15, ORDINAL1:def 12; :: thesis: verum
end;
now :: thesis: 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) < r
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
dist (((x * N) . m),z) < r )
assume A10: 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist (((x * N) . m),z) < r
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
dist (((x * N) . m),z) < r
thus for m being Nat st n <= m holds
dist (((x * N) . m),z) < r :: thesis: verum
proof
let m be Nat; :: thesis: ( n <= m implies dist (((x * N) . m),z) < r )
assume n <= m ; :: thesis: dist (((x * N) . m),z) < r
dist (((x * N) . m),z) = dist (z,z) by A9
.= 0 by METRIC_1:1 ;
hence dist (((x * N) . m),z) < r by A10; :: thesis: verum
end;
end;
hence ( ex N being increasing sequence of NAT st x * N = x * N & x * N is convergent & lim (x * N) in [#] M ) ; :: thesis: verum
end;
suppose rng x is infinite ; :: thesis: 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; :: thesis: for ix being Element of NAT ex iy being Element of NAT st S1[n,ix,iy]
let ix be Element of NAT ; :: thesis: 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] ; :: thesis: 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))
proof
let g be object ; :: thesis: ( g in (Ball (z,(1 / (2 + n)))) /\ ((rng x) \ {z}) implies g in x .: (Segm (ix + 1)) )
assume A18: g in (Ball (z,(1 / (2 + n)))) /\ ((rng x) \ {z}) ; :: thesis: g in x .: (Segm (ix + 1))
then ( g in Ball (z,(1 / (2 + n))) & g in (rng x) \ {z} ) by XBOOLE_0:def 4;
then g in rng x by XBOOLE_0:def 5;
then consider iy being Element of NAT such that
A19: g = x . iy by FUNCT_2:113;
iy <= ix by A16, A17, A18, A19;
then iy < ix + 1 by NAT_1:13;
then iy in Segm (ix + 1) by NAT_1:44;
hence g in x .: (Segm (ix + 1)) by A19, FUNCT_2:35; :: thesis: verum
end;
then (Ball (z,(1 / (2 + n)))) /\ ((rng x) \ {z}) c= x .: (Segm (ix + 1)) by TARSKI:def 3;
hence contradiction by A12, LM3; :: thesis: 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; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
( N . k < N . (k + 1) & x . (N . (k + 1)) in Ball (z,(1 / (2 + k))) ) by A20;
hence S2[k + 1] ; :: thesis: verum
end;
A23: for i being Nat holds S2[i] from NAT_1:sch 2(A21, A22);
now :: thesis: 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) < r
let r be Real; :: thesis: ( 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 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist (((x * N) . m),z) < r
consider 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; :: thesis: for m being Nat st n <= m holds
dist (((x * N) . m),z) < r
thus for m being Nat st n <= m holds
dist (((x * N) . m),z) < r :: thesis: verum
proof
let m be Nat; :: thesis: ( n <= m implies dist (((x * N) . m),z) < r )
assume n <= m ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
end;
end;
then [#] M is sequentially_compact ;
hence M is sequentially_compact ; :: thesis: verum