let M be non empty MetrSpace; :: thesis: for A being non empty Subset of M
for S being sequence of (M | A)
for S' being sequence of M st S = S' holds
( S' is Cauchy iff S is Cauchy )
let A be non empty Subset of M; :: thesis: for S being sequence of (M | A)
for S' being sequence of M st S = S' holds
( S' is Cauchy iff S is Cauchy )
let S be sequence of (M | A); :: thesis: for S' being sequence of M st S = S' holds
( S' is Cauchy iff S is Cauchy )
let S' be sequence of M; :: thesis: ( S = S' implies ( S' is Cauchy iff S is Cauchy ) )
assume A1:
S = S'
; :: thesis: ( S' is Cauchy iff S is Cauchy )
thus
( S' is Cauchy implies S is Cauchy )
:: thesis: ( S is Cauchy implies S' is Cauchy )proof
assume A2:
S' is
Cauchy
;
:: thesis: S is Cauchy
let r be
Real;
:: according to TBSP_1:def 5 :: thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist (S . b2),(S . b3) ) )
assume A3:
r > 0
;
:: thesis: ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist (S . b2),(S . b3) )
consider p being
Element of
NAT such that A4:
for
n,
m being
Element of
NAT st
p <= n &
p <= m holds
dist (S' . n),
(S' . m) < r
by A2, A3, TBSP_1:def 5;
take
p
;
:: thesis: for b1, b2 being Element of NAT holds
( not p <= b1 or not p <= b2 or not r <= dist (S . b1),(S . b2) )
let n,
m be
Element of
NAT ;
:: thesis: ( not p <= n or not p <= m or not r <= dist (S . n),(S . m) )
assume A5:
(
p <= n &
p <= m )
;
:: thesis: not r <= dist (S . n),(S . m)
dist (S . n),
(S . m) = dist (S' . n),
(S' . m)
by A1, TOPMETR:def 1;
hence
not
r <= dist (S . n),
(S . m)
by A4, A5;
:: thesis: verum
end;
assume A6:
S is Cauchy
; :: thesis: S' is Cauchy
let r be Real; :: according to TBSP_1:def 5 :: thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist (S' . b2),(S' . b3) ) )
assume A7:
r > 0
; :: thesis: ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist (S' . b2),(S' . b3) )
consider p being Element of NAT such that
A8:
for n, m being Element of NAT st p <= n & p <= m holds
dist (S . n),(S . m) < r
by A6, A7, TBSP_1:def 5;
take
p
; :: thesis: for b1, b2 being Element of NAT holds
( not p <= b1 or not p <= b2 or not r <= dist (S' . b1),(S' . b2) )
let n, m be Element of NAT ; :: thesis: ( not p <= n or not p <= m or not r <= dist (S' . n),(S' . m) )
assume A9:
( p <= n & p <= m )
; :: thesis: not r <= dist (S' . n),(S' . m)
dist (S . n),(S . m) = dist (S' . n),(S' . m)
by A1, TOPMETR:def 1;
hence
not r <= dist (S' . n),(S' . m)
by A8, A9; :: thesis: verum