let X be RealUnitarySpace; for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
let seq be sequence of X; ( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
thus
( seq is Cauchy implies for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy )
( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy )
proof
assume A3:
for
r being
Real st
r > 0 holds
ex
k being
Nat st
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((seq . n) - (seq . m)).|| < r
;
seq is Cauchy
let r be
Real;
BHSP_3:def 1 ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r )
assume
r > 0
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
then consider l being
Nat such that A4:
for
n,
m being
Nat st
n >= l &
m >= l holds
||.((seq . n) - (seq . m)).|| < r
by A3;
take k =
l;
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
let n,
m be
Nat;
( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r )
assume
(
n >= k &
m >= k )
;
dist ((seq . n),(seq . m)) < r
then
||.((seq . n) - (seq . m)).|| < r
by A4;
hence
dist (
(seq . n),
(seq . m))
< r
by BHSP_1:def 5;
verum
end;
hence
( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy )
; verum