:: Cauchy Sequence of Complex Unitary Space
:: by Yasumasa Suzuki and Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users
deffunc H1( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;
definition
canceled;
end;
:: deftheorem CLVECT_3:def 1 :
canceled;
theorem Th1: :: CLVECT_3:1
theorem Th2: :: CLVECT_3:2
theorem Th3: :: CLVECT_3:3
theorem :: CLVECT_3:4
theorem :: CLVECT_3:5
:: deftheorem Def2 defines summable CLVECT_3:def 2 :
:: deftheorem defines Sum CLVECT_3:def 3 :
theorem :: CLVECT_3:6
theorem :: CLVECT_3:7
theorem :: CLVECT_3:8
theorem Th9: :: CLVECT_3:9
theorem Th10: :: CLVECT_3:10
theorem :: CLVECT_3:11
theorem Th12: :: CLVECT_3:12
theorem Th13: :: CLVECT_3:13
theorem :: CLVECT_3:14
:: deftheorem defines Sum CLVECT_3:def 4 :
theorem :: CLVECT_3:15
theorem Th16: :: CLVECT_3:16
theorem Th17: :: CLVECT_3:17
theorem :: CLVECT_3:18
theorem Th19: :: CLVECT_3:19
theorem :: CLVECT_3:20
:: deftheorem defines Sum CLVECT_3:def 5 :
theorem :: CLVECT_3:21
theorem :: CLVECT_3:22
theorem Th23: :: CLVECT_3:23
theorem :: CLVECT_3:24
:: deftheorem defines Sum CLVECT_3:def 6 :
:: deftheorem defines Sum CLVECT_3:def 7 :
:: deftheorem Def8 defines absolutely_summable CLVECT_3:def 8 :
theorem :: CLVECT_3:25
theorem :: CLVECT_3:26
theorem :: CLVECT_3:27
theorem :: CLVECT_3:28
theorem Th29: :: CLVECT_3:29
theorem Th30: :: CLVECT_3:30
theorem :: CLVECT_3:31
theorem :: CLVECT_3:32
theorem :: CLVECT_3:33
theorem :: CLVECT_3:34
theorem Th35: :: CLVECT_3:35
theorem :: CLVECT_3:36
theorem Th37: :: CLVECT_3:37
theorem :: CLVECT_3:38
theorem Th39: :: CLVECT_3:39
theorem Th40: :: CLVECT_3:40
theorem :: CLVECT_3:41
theorem :: CLVECT_3:42
:: deftheorem Def9 defines * CLVECT_3:def 9 :
theorem :: CLVECT_3:43
theorem :: CLVECT_3:44
theorem :: CLVECT_3:45
theorem Th46: :: CLVECT_3:46
theorem :: CLVECT_3:47
Lm1:
for s being Complex_Sequence st s is convergent holds
s is bounded
theorem Th48: :: CLVECT_3:48
theorem :: CLVECT_3:49
theorem :: CLVECT_3:50
:: deftheorem Def10 defines Cauchy CLVECT_3:def 10 :
theorem :: CLVECT_3:51
theorem Th52: :: CLVECT_3:52
theorem Th53: :: CLVECT_3:53
theorem :: CLVECT_3:54