let X be ComplexHilbertSpace; for seq being sequence of X holds
( seq is summable 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
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
let seq be sequence of X; ( seq is summable 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
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
thus
( seq is summable 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
||.((Sum (seq,n)) - (Sum (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
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) implies seq is summable )proof
assume A1:
seq is
summable
;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
now for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < rlet r be
Real;
( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )assume
r > 0
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < rthen consider k being
Nat such that A2:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
by A1, Th10;
take k =
k;
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < rlet n,
m be
Nat;
( n >= k & m >= k implies ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )assume
(
n >= k &
m >= k )
;
||.((Sum (seq,n)) - (Sum (seq,m))).|| < rhence
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
by A2;
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
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
;
verum
end;
thus
( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ) implies seq is summable )
verum