begin
deffunc H1( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def1 defines convergent CLVECT_2:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def2 defines lim CLVECT_2:def 2 :
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
:: deftheorem Def3 defines ||. CLVECT_2:def 3 :
theorem Th20:
theorem Th21:
theorem Th22:
:: deftheorem Def4 defines dist CLVECT_2:def 4 :
theorem Th23:
theorem Th24:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm1:
for X being ComplexUnitarySpace
for g, x being Point of
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
theorem Th33:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Ball CLVECT_2:def 5 :
:: deftheorem defines cl_Ball CLVECT_2:def 6 :
:: deftheorem defines Sphere CLVECT_2:def 7 :
theorem Th40:
theorem Th41:
theorem
theorem
theorem
theorem
theorem
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem Th51:
theorem
theorem
theorem Th54:
theorem Th55:
theorem
begin
deffunc H2( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def8 defines Cauchy CLVECT_2:def 8 :
theorem
theorem
theorem
theorem
theorem Th61:
theorem
theorem Th63:
theorem
theorem
:: deftheorem Def9 defines is_compared_to CLVECT_2:def 9 :
theorem Th66:
theorem Th67:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def10 defines bounded CLVECT_2:def 10 :
theorem Th74:
theorem Th75:
theorem
theorem
theorem
theorem Th79:
theorem Th80:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th94:
theorem Th95:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem CLVECT_2:def 11 :
canceled;
:: deftheorem Def12 defines complete CLVECT_2:def 12 :
theorem
:: deftheorem defines Hilbert CLVECT_2:def 13 :