:: Introduction to Banach and Hilbert spaces - Part II
:: 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 convergent BHSP_2:def 1 :
theorem Th1: :: BHSP_2:1
theorem Th2: :: BHSP_2:2
theorem Th3: :: BHSP_2:3
theorem Th4: :: BHSP_2:4
theorem Th5: :: BHSP_2:5
theorem Th6: :: BHSP_2:6
theorem Th7: :: BHSP_2:7
theorem Th8: :: BHSP_2:8
theorem Th9: :: BHSP_2:9
:: deftheorem Def2 defines lim BHSP_2:def 2 :
theorem Th10: :: BHSP_2:10
theorem :: BHSP_2:11
theorem :: BHSP_2:12
theorem Th13: :: BHSP_2:13
theorem Th14: :: BHSP_2:14
theorem Th15: :: BHSP_2:15
theorem Th16: :: BHSP_2:16
theorem Th17: :: BHSP_2:17
theorem :: BHSP_2:18
theorem Th19: :: BHSP_2:19
:: deftheorem Def3 defines ||. BHSP_2:def 3 :
theorem Th20: :: BHSP_2:20
theorem Th21: :: BHSP_2:21
theorem Th22: :: BHSP_2:22
:: deftheorem Def4 defines dist BHSP_2:def 4 :
theorem Th23: :: BHSP_2:23
theorem Th24: :: BHSP_2:24
theorem :: BHSP_2:25
theorem :: BHSP_2:26
theorem :: BHSP_2:27
theorem :: BHSP_2:28
theorem :: BHSP_2:29
theorem :: BHSP_2:30
theorem :: BHSP_2:31
theorem :: BHSP_2:32
Lm1:
for X being RealUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
theorem Th33: :: BHSP_2:33
theorem :: BHSP_2:34
theorem :: BHSP_2:35
theorem :: BHSP_2:36
theorem :: BHSP_2:37
theorem :: BHSP_2:38
theorem :: BHSP_2:39
:: deftheorem defines Ball BHSP_2:def 5 :
:: deftheorem defines cl_Ball BHSP_2:def 6 :
:: deftheorem defines Sphere BHSP_2:def 7 :
theorem Th40: :: BHSP_2:40
theorem Th41: :: BHSP_2:41
theorem :: BHSP_2:42
theorem :: BHSP_2:43
theorem :: BHSP_2:44
theorem :: BHSP_2:45
theorem :: BHSP_2:46
theorem Th47: :: BHSP_2:47
theorem Th48: :: BHSP_2:48
theorem :: BHSP_2:49
theorem Th50: :: BHSP_2:50
theorem Th51: :: BHSP_2:51
theorem :: BHSP_2:52
theorem :: BHSP_2:53
theorem Th54: :: BHSP_2:54
theorem Th55: :: BHSP_2:55
theorem :: BHSP_2:56