let M be non empty MetrSpace; ( M is sequentially_compact implies ( M is totally_bounded & M is complete ) )
assume
M is sequentially_compact
; ( M is totally_bounded & M is complete )
then A1:
[#] M is sequentially_compact
;
thus
M is totally_bounded
M is complete proof
assume
not
M is
totally_bounded
;
contradiction
then consider r being
Real such that A2:
(
r > 0 & ( for
G being
Subset-Family of
M holds
( not
G is
finite or not the
carrier of
M = union G or ex
C being
Subset of
M st
(
C in G & ( for
w being
Element of
M holds not
C = Ball (
w,
r) ) ) ) ) )
;
set S0 = the
Element of
M;
set G0 =
{} ;
set ABL =
{ GX where GX is Subset-Family of M : ( GX is finite & ( for C being Subset of M st C in GX holds
ex w being Element of M st C = Ball (w,r) ) ) } ;
A3:
{} is
Subset of
(bool ([#] M))
by XBOOLE_1:2;
for
C being
Subset of
M st
C in {} holds
ex
w being
Element of
M st
C = Ball (
w,
r)
;
then A4:
{} in { GX where GX is Subset-Family of M : ( GX is finite & ( for C being Subset of M st C in GX holds
ex w being Element of M st C = Ball (w,r) ) ) }
by A3;
then reconsider ABL =
{ GX where GX is Subset-Family of M : ( GX is finite & ( for C being Subset of M st C in GX holds
ex w being Element of M st C = Ball (w,r) ) ) } as non
empty set ;
reconsider G0 =
{} as
Element of
ABL by A4;
defpred S1[
Nat,
Element of
M,
set ,
Element of
M,
set ]
means ( $5
= $3
\/ {(Ball ($2,r))} & not $4
in union $5 );
A5:
for
n being
Nat for
x being
Element of
M for
y being
Element of
ABL ex
x1 being
Element of
M ex
y1 being
Element of
ABL st
S1[
n,
x,
y,
x1,
y1]
proof
let n be
Nat;
for x being Element of M
for y being Element of ABL ex x1 being Element of M ex y1 being Element of ABL st S1[n,x,y,x1,y1]let x be
Element of
M;
for y being Element of ABL ex x1 being Element of M ex y1 being Element of ABL st S1[n,x,y,x1,y1]let y be
Element of
ABL;
ex x1 being Element of M ex y1 being Element of ABL st S1[n,x,y,x1,y1]
y in ABL
;
then consider GX being
Subset-Family of
M such that A6:
(
y = GX &
GX is
finite & ( for
C being
Subset of
M st
C in GX holds
ex
w being
Element of
M st
C = Ball (
w,
r) ) )
;
set y1 =
y \/ {(Ball (x,r))};
Ball (
x,
r)
in bool ([#] M)
by ZFMISC_1:def 1;
then
{(Ball (x,r))} c= bool ([#] M)
by ZFMISC_1:31;
then reconsider y1 =
y \/ {(Ball (x,r))} as
Subset-Family of
M by A6, XBOOLE_1:8;
A7:
for
C being
Subset of
M st
C in y1 holds
ex
w being
Element of
M st
C = Ball (
w,
r)
then A8:
y1 in ABL
by A6;
not the
carrier of
M = union y1
by A2, A6, A7;
then consider x1 being
object such that A9:
(
x1 in the
carrier of
M & not
x1 in union y1 )
by TARSKI:def 3;
reconsider x1 =
x1 as
Element of
M by A9;
reconsider y1 =
y1 as
Element of
ABL by A8;
take
x1
;
ex y1 being Element of ABL st S1[n,x,y,x1,y1]
take
y1
;
S1[n,x,y,x1,y1]
thus
S1[
n,
x,
y,
x1,
y1]
by A9;
verum
end;
consider S1 being
sequence of
M,
Y being
sequence of
ABL such that A10:
(
S1 . 0 = the
Element of
M &
Y . 0 = G0 & ( for
n being
Nat holds
S1[
n,
S1 . n,
Y . n,
S1 . (n + 1),
Y . (n + 1)] ) )
from RECDEF_2:sch 3(A5);
rng S1 c= [#] M
;
then consider S2 being
sequence of
M such that A11:
( ex
N being
increasing sequence of
NAT st
S2 = S1 * N &
S2 is
convergent &
lim S2 in [#] M )
by A1;
defpred S2[
Nat]
means for
k being
Nat st
k <= $1 holds
Ball (
(S1 . k),
r)
c= union (Y . ($1 + 1));
A12:
S2[
0 ]
A14:
for
n being
Nat st
S2[
n] holds
S2[
n + 1]
A19:
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A12, A14);
A20:
for
n,
k being
Nat st
k <= n holds
r <= dist (
(S1 . (n + 1)),
(S1 . k))
A21:
for
n,
k being
Nat st
k < n holds
r <= dist (
(S1 . n),
(S1 . k))
not
S2 is
convergent
hence
contradiction
by A11;
verum
end;
now for S being sequence of M st S is Cauchy holds
S is convergent let S be
sequence of
M;
( S is Cauchy implies S is convergent )assume A28:
S is
Cauchy
;
S is convergent thus
S is
convergent
verumproof
reconsider S1 =
S as
sequence of
([#] M) ;
rng S1 c= [#] M
;
then consider S2 being
sequence of
M such that A29:
( ex
N being
increasing sequence of
NAT st
S2 = S1 * N &
S2 is
convergent &
lim S2 in [#] M )
by A1;
consider N being
increasing sequence of
NAT such that A30:
S2 = S1 * N
by A29;
take x =
lim S2;
TBSP_1:def 2 for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= dist ((S . b3),x) ) )
let r be
Real;
( r <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not r <= dist ((S . b2),x) ) )
assume A31:
0 < r
;
ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not r <= dist ((S . b2),x) )
then consider p being
Nat such that A32:
for
n,
m being
Nat st
p <= n &
p <= m holds
dist (
(S . n),
(S . m))
< r / 2
by A28;
consider q being
Nat such that A33:
for
m being
Nat st
m >= q holds
dist (
(S2 . m),
(lim S2))
< r / 2
by A29, A31, TBSP_1:def 3;
reconsider l =
max (
p,
q) as
Nat by XXREAL_0:16;
take
l
;
for b1 being set holds
( not l <= b1 or not r <= dist ((S . b1),x) )
let m be
Nat;
( not l <= m or not r <= dist ((S . m),x) )
assume A34:
l <= m
;
not r <= dist ((S . m),x)
p <= l
by XXREAL_0:25;
then A35:
p <= m
by A34, XXREAL_0:2;
m <= N . m
by SEQM_3:14;
then
p <= N . m
by A35, XXREAL_0:2;
then
dist (
(S . m),
(S . (N . m)))
< r / 2
by A32, A35;
then A36:
dist (
(S . m),
(S2 . m))
< r / 2
by A30, FUNCT_2:15, ORDINAL1:def 12;
q <= l
by XXREAL_0:25;
then
q <= m
by A34, XXREAL_0:2;
then
dist (
(S2 . m),
(lim S2))
< r / 2
by A33;
then A37:
(dist ((S . m),(S2 . m))) + (dist ((S2 . m),(lim S2))) < (r / 2) + (r / 2)
by A36, XREAL_1:8;
dist (
(S . m),
x)
<= (dist ((S . m),(S2 . m))) + (dist ((S2 . m),x))
by METRIC_1:4;
hence
not
r <= dist (
(S . m),
x)
by A37, XXREAL_0:2;
verum
end; end;
hence
M is complete
; verum