begin
deffunc H1( ComplexUnitarySpace) -> Element of the U1 of $1 = 0. $1;
definition
canceled;
end;
:: deftheorem CLVECT_3:def 1 :
canceled;
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
:: deftheorem Def2 defines summable CLVECT_3:def 2 :
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );
:: deftheorem defines Sum CLVECT_3:def 3 :
for X being ComplexUnitarySpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);
theorem
theorem
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
:: deftheorem defines Sum CLVECT_3:def 4 :
for X being ComplexUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum seq,n = (Partial_Sums seq) . n;
theorem
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem
:: deftheorem defines Sum CLVECT_3:def 5 :
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds Sum seq,n,m = (Sum seq,n) - (Sum seq,m);
theorem
theorem
theorem Th23:
theorem
:: deftheorem defines Sum CLVECT_3:def 6 :
for Cseq being Complex_Sequence
for n being Element of NAT holds Sum Cseq,n = (Partial_Sums Cseq) . n;
:: deftheorem defines Sum CLVECT_3:def 7 :
for Cseq being Complex_Sequence
for n, m being Element of NAT holds Sum Cseq,n,m = (Sum Cseq,n) - (Sum Cseq,m);
:: deftheorem Def8 defines absolutely_summable CLVECT_3:def 8 :
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is absolutely_summable iff ||.seq.|| is summable );
theorem
theorem
theorem
theorem
theorem Th29:
theorem Th30:
theorem
theorem
theorem
theorem
theorem Th35:
theorem
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem
theorem
:: deftheorem Def9 defines * CLVECT_3:def 9 :
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for b4 being sequence of X holds
( b4 = Cseq * seq iff for n being Element of NAT holds b4 . n = (Cseq . n) * (seq . n) );
theorem
theorem
theorem
theorem Th46:
theorem
Lm1:
for s being Complex_Sequence st s is convergent holds
s is bounded
theorem Th48:
theorem
theorem
:: deftheorem Def10 defines Cauchy CLVECT_3:def 10 :
for Cseq being Complex_Sequence holds
( Cseq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r );
theorem
theorem Th52:
theorem Th53:
theorem