let X be non empty MetrSpace; for S, S1 being sequence of X st S is Cauchy & S1 is subsequence of S holds
S1 is Cauchy
let S, S1 be sequence of X; ( S is Cauchy & S1 is subsequence of S implies S1 is Cauchy )
assume that
A1:
S is Cauchy
and
A2:
S1 is subsequence of S
; S1 is Cauchy
consider Nseq being increasing sequence of NAT such that
A3:
S1 = S * Nseq
by A2, VALUED_0:def 17;
for r being Real st 0 < r holds
ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
proof
let r be
Real;
( 0 < r implies ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r )
assume
0 < r
;
ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
then consider m1 being
Element of
NAT such that A4:
for
n,
k being
Element of
NAT st
m1 <= n &
m1 <= k holds
dist (
(S . n),
(S . k))
< r
by A1, TBSP_1:def 4;
take m =
m1;
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
for
n,
k being
Element of
NAT st
m <= n &
m <= k holds
dist (
(S1 . n),
(S1 . k))
< r
proof
let n,
k be
Element of
NAT ;
( m <= n & m <= k implies dist ((S1 . n),(S1 . k)) < r )
assume that A5:
m <= n
and A6:
m <= k
;
dist ((S1 . n),(S1 . k)) < r
k <= Nseq . k
by SEQM_3:14;
then A7:
m1 <= Nseq . k
by A6, XXREAL_0:2;
dom S = NAT
by FUNCT_2:def 1;
then
(
dom Nseq = NAT &
Nseq . k in dom S )
by FUNCT_2:def 1;
then
k in dom (S * Nseq)
by FUNCT_1:11;
then A8:
S1 . k = S . (Nseq . k)
by A3, FUNCT_1:12;
dom S = NAT
by FUNCT_2:def 1;
then
(
dom Nseq = NAT &
Nseq . n in dom S )
by FUNCT_2:def 1;
then
n in dom (S * Nseq)
by FUNCT_1:11;
then A9:
S1 . n = S . (Nseq . n)
by A3, FUNCT_1:12;
n <= Nseq . n
by SEQM_3:14;
then
m1 <= Nseq . n
by A5, XXREAL_0:2;
hence
dist (
(S1 . n),
(S1 . k))
< r
by A4, A9, A7, A8;
verum
end;
hence
for
n,
k being
Element of
NAT st
m <= n &
m <= k holds
dist (
(S1 . n),
(S1 . k))
< r
;
verum
end;
hence
S1 is Cauchy
by TBSP_1:def 4; verum