:: Series on Complex {B}anach Algebra
:: by Noboru Endou
::
:: Received April 6, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: CLOPBAN3:1
:: deftheorem CLOPBAN3:def 1 :
canceled;
:: deftheorem Def2 defines summable CLOPBAN3:def 2 :
:: deftheorem defines Sum CLOPBAN3:def 3 :
:: deftheorem Def4 defines norm_summable CLOPBAN3:def 4 :
theorem Th2: :: CLOPBAN3:2
theorem Th3: :: CLOPBAN3:3
theorem Th4: :: CLOPBAN3:4
theorem Th5: :: CLOPBAN3:5
theorem Th6: :: CLOPBAN3:6
theorem :: CLOPBAN3:7
canceled;
theorem :: CLOPBAN3:8
canceled;
theorem :: CLOPBAN3:9
canceled;
theorem Th10: :: CLOPBAN3:10
theorem Th11: :: CLOPBAN3:11
theorem :: CLOPBAN3:12
canceled;
theorem Th13: :: CLOPBAN3:13
theorem Th14: :: CLOPBAN3:14
theorem Th15: :: CLOPBAN3:15
theorem Th16: :: CLOPBAN3:16
theorem Th17: :: CLOPBAN3:17
theorem Th18: :: CLOPBAN3:18
theorem Th19: :: CLOPBAN3:19
theorem Th20: :: CLOPBAN3:20
theorem Th21: :: CLOPBAN3:21
theorem Th22: :: CLOPBAN3:22
theorem Th23: :: CLOPBAN3:23
theorem Th24: :: CLOPBAN3:24
theorem Th25: :: CLOPBAN3:25
theorem Th26: :: CLOPBAN3:26
theorem Th27: :: CLOPBAN3:27
theorem Th28: :: CLOPBAN3:28
theorem Th29: :: CLOPBAN3:29
theorem Th30: :: CLOPBAN3:30
theorem :: CLOPBAN3:31
theorem :: CLOPBAN3:32
theorem :: CLOPBAN3:33
theorem :: CLOPBAN3:34
theorem :: CLOPBAN3:35
theorem :: CLOPBAN3:36
theorem :: CLOPBAN3:37
theorem :: CLOPBAN3:38
theorem :: CLOPBAN3:39
theorem :: CLOPBAN3:40
theorem :: CLOPBAN3:41
theorem Th42: :: CLOPBAN3:42
:: deftheorem CLOPBAN3:def 5 :
canceled;
:: deftheorem CLOPBAN3:def 6 :
canceled;
:: deftheorem CLOPBAN3:def 7 :
canceled;
:: deftheorem defines * CLOPBAN3:def 8 :
:: deftheorem defines * CLOPBAN3:def 9 :
:: deftheorem defines * CLOPBAN3:def 10 :
:: deftheorem CLOPBAN3:def 11 :
canceled;
:: deftheorem Def12 defines GeoSeq CLOPBAN3:def 12 :
:: deftheorem defines #N CLOPBAN3:def 13 :
theorem :: CLOPBAN3:43
theorem Th44: :: CLOPBAN3:44
theorem :: CLOPBAN3:45
Lm4:
for X being ComplexNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
Lm5:
for X being ComplexNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
Lm6:
for X being ComplexNormSpace
for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds
x = y
theorem :: CLOPBAN3:46