:: The Series on {B}anach Algebra
:: by Yasunari Shidama
::
:: Received February 3, 2004
:: Copyright (c) 2004 Association of Mizar Users
definition
canceled;
end;
:: deftheorem LOPBAN_3:def 1 :
canceled;
theorem Th1: :: LOPBAN_3:1
:: deftheorem Def2 defines summable LOPBAN_3:def 2 :
:: deftheorem defines Sum LOPBAN_3:def 3 :
:: deftheorem Def4 defines norm_summable LOPBAN_3:def 4 :
theorem Th2: :: LOPBAN_3:2
theorem Th3: :: LOPBAN_3:3
theorem Th4: :: LOPBAN_3:4
theorem Th5: :: LOPBAN_3:5
theorem Th6: :: LOPBAN_3:6
theorem :: LOPBAN_3:7
canceled;
theorem :: LOPBAN_3:8
canceled;
theorem :: LOPBAN_3:9
canceled;
theorem :: LOPBAN_3:10
canceled;
theorem Th11: :: LOPBAN_3:11
theorem Th12: :: LOPBAN_3:12
theorem :: LOPBAN_3:13
canceled;
theorem Th14: :: LOPBAN_3:14
theorem Th15: :: LOPBAN_3:15
theorem Th16: :: LOPBAN_3:16
theorem Th17: :: LOPBAN_3:17
theorem Th18: :: LOPBAN_3:18
theorem Th19: :: LOPBAN_3:19
theorem Th20: :: LOPBAN_3:20
theorem Th21: :: LOPBAN_3:21
theorem Th22: :: LOPBAN_3:22
theorem Th23: :: LOPBAN_3:23
theorem Th24: :: LOPBAN_3:24
theorem Th25: :: LOPBAN_3:25
theorem Th26: :: LOPBAN_3:26
theorem Th27: :: LOPBAN_3:27
theorem Th28: :: LOPBAN_3:28
theorem Th29: :: LOPBAN_3:29
theorem Th30: :: LOPBAN_3:30
theorem Th31: :: LOPBAN_3:31
theorem :: LOPBAN_3:32
theorem :: LOPBAN_3:33
theorem :: LOPBAN_3:34
theorem :: LOPBAN_3:35
theorem :: LOPBAN_3:36
theorem :: LOPBAN_3:37
theorem :: LOPBAN_3:38
theorem :: LOPBAN_3:39
theorem :: LOPBAN_3:40
theorem :: LOPBAN_3:41
theorem :: LOPBAN_3:42
theorem Th43: :: LOPBAN_3:43
:: deftheorem LOPBAN_3:def 5 :
canceled;
:: deftheorem LOPBAN_3:def 6 :
canceled;
:: deftheorem LOPBAN_3:def 7 :
canceled;
:: deftheorem Def8 defines invertible LOPBAN_3:def 8 :
:: deftheorem defines * LOPBAN_3:def 9 :
:: deftheorem defines * LOPBAN_3:def 10 :
:: deftheorem defines * LOPBAN_3:def 11 :
:: deftheorem Def12 defines " LOPBAN_3:def 12 :
:: deftheorem Def13 defines GeoSeq LOPBAN_3:def 13 :
:: deftheorem defines #N LOPBAN_3:def 14 :
theorem :: LOPBAN_3:44
theorem Th45: :: LOPBAN_3:45
theorem :: LOPBAN_3:46
Lm4:
for X being RealNormSpace
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 RealNormSpace
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 RealNormSpace
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 :: LOPBAN_3:47