:: Introduction to Banach and Hilbert spaces - Part III
:: by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991 Association of Mizar Users
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def1 defines Cauchy BHSP_3:def 1 :
theorem :: BHSP_3:1
theorem :: BHSP_3:2
theorem :: BHSP_3:3
theorem :: BHSP_3:4
theorem Th5: :: BHSP_3:5
theorem :: BHSP_3:6
theorem Th7: :: BHSP_3:7
theorem :: BHSP_3:8
theorem :: BHSP_3:9
:: deftheorem Def2 defines is_compared_to BHSP_3:def 2 :
theorem Th10: :: BHSP_3:10
theorem Th11: :: BHSP_3:11
theorem :: BHSP_3:12
theorem :: BHSP_3:13
theorem :: BHSP_3:14
theorem :: BHSP_3:15
theorem :: BHSP_3:16
theorem :: BHSP_3:17
:: deftheorem Def3 defines bounded BHSP_3:def 3 :
theorem Th18: :: BHSP_3:18
theorem Th19: :: BHSP_3:19
theorem :: BHSP_3:20
theorem :: BHSP_3:21
theorem :: BHSP_3:22
theorem Th23: :: BHSP_3:23
theorem Th24: :: BHSP_3:24
theorem :: BHSP_3:25
theorem :: BHSP_3:26
canceled;
theorem :: BHSP_3:27
canceled;
theorem :: BHSP_3:28
canceled;
theorem :: BHSP_3:29
canceled;
theorem :: BHSP_3:30
canceled;
theorem Th31: :: BHSP_3:31
theorem Th32: :: BHSP_3:32
theorem Th33: :: BHSP_3:33
theorem Th34: :: BHSP_3:34
theorem :: BHSP_3:35
canceled;
theorem :: BHSP_3:36
theorem :: BHSP_3:37
theorem Th38: :: BHSP_3:38
theorem Th39: :: BHSP_3:39
theorem :: BHSP_3:40
theorem :: BHSP_3:41
theorem :: BHSP_3:42
canceled;
theorem :: BHSP_3:43
canceled;
theorem :: BHSP_3:44
theorem :: BHSP_3:45
canceled;
theorem :: BHSP_3:46
theorem :: BHSP_3:47
theorem :: BHSP_3:48
theorem :: BHSP_3:49
theorem :: BHSP_3:50
theorem :: BHSP_3:51
:: deftheorem BHSP_3:def 4 :
canceled;
:: deftheorem BHSP_3:def 5 :
canceled;
:: deftheorem Def6 defines complete BHSP_3:def 6 :
theorem :: BHSP_3:52
canceled;
theorem :: BHSP_3:53
:: deftheorem defines Hilbert BHSP_3:def 7 :