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 Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
proof
let r be
Real;
( 0 < r implies ex m being Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r )
assume
0 < r
;
ex m being Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
then consider m1 being
Nat such that A4:
for
n,
k being
Nat st
m1 <= n &
m1 <= k holds
dist (
(S . n),
(S . k))
< r
by A1;
take m =
m1;
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
for
n,
k being
Nat st
m <= n &
m <= k holds
dist (
(S1 . n),
(S1 . k))
< r
proof
let n,
k be
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;
A8:
k in NAT
by ORDINAL1:def 12;
A9:
n in NAT
by ORDINAL1:def 12;
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, A8;
then A10:
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, A9;
then A11:
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, A11, A7, A10;
verum
end;
hence
for
n,
k being
Nat st
m <= n &
m <= k holds
dist (
(S1 . n),
(S1 . k))
< r
;
verum
end;
hence
S1 is Cauchy
; verum