:: Series in Banach and Hilbert Spaces
:: by El\.zbieta Kraszewska and Jan Popio{\l}ek
::
:: Received April 1, 1992
:: Copyright (c) 1992 Association of Mizar Users
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def1 defines Partial_Sums BHSP_4:def 1 :
theorem Th1: :: BHSP_4:1
theorem Th2: :: BHSP_4:2
theorem Th3: :: BHSP_4:3
theorem :: BHSP_4:4
theorem :: BHSP_4:5
:: deftheorem Def2 defines summable BHSP_4:def 2 :
:: deftheorem defines Sum BHSP_4:def 3 :
theorem :: BHSP_4:6
theorem :: BHSP_4:7
theorem :: BHSP_4:8
theorem Th9: :: BHSP_4:9
theorem Th10: :: BHSP_4:10
theorem :: BHSP_4:11
theorem Th12: :: BHSP_4:12
theorem Th13: :: BHSP_4:13
theorem :: BHSP_4:14
:: deftheorem defines Sum BHSP_4:def 4 :
theorem :: BHSP_4:15
canceled;
theorem :: BHSP_4:16
theorem Th17: :: BHSP_4:17
theorem Th18: :: BHSP_4:18
theorem :: BHSP_4:19
theorem Th20: :: BHSP_4:20
theorem :: BHSP_4:21
:: deftheorem defines Sum BHSP_4:def 5 :
theorem :: BHSP_4:22
canceled;
theorem :: BHSP_4:23
theorem :: BHSP_4:24
theorem Th25: :: BHSP_4:25
theorem :: BHSP_4:26
:: deftheorem BHSP_4:def 6 :
canceled;
:: deftheorem BHSP_4:def 7 :
canceled;
:: deftheorem Def8 defines absolutely_summable BHSP_4:def 8 :
theorem :: BHSP_4:27
theorem :: BHSP_4:28
theorem :: BHSP_4:29
theorem :: BHSP_4:30
theorem Th31: :: BHSP_4:31
theorem Th32: :: BHSP_4:32
theorem :: BHSP_4:33
theorem :: BHSP_4:34
theorem :: BHSP_4:35
theorem :: BHSP_4:36
theorem Th37: :: BHSP_4:37
theorem :: BHSP_4:38
theorem Th39: :: BHSP_4:39
theorem :: BHSP_4:40
theorem Th41: :: BHSP_4:41
theorem :: BHSP_4:42
theorem :: BHSP_4:43
theorem :: BHSP_4:44
:: deftheorem Def9 defines * BHSP_4:def 9 :
theorem :: BHSP_4:45
theorem :: BHSP_4:46
theorem :: BHSP_4:47
theorem Th48: :: BHSP_4:48
theorem :: BHSP_4:49
theorem Th50: :: BHSP_4:50
theorem :: BHSP_4:51
theorem :: BHSP_4:52
:: deftheorem Def10 defines Cauchy BHSP_4:def 10 :
theorem :: BHSP_4:53
theorem Th54: :: BHSP_4:54
theorem Th55: :: BHSP_4:55
theorem :: BHSP_4:56