:: Convergent Sequences in Complex Unitary Space
:: by Noboru Endou
::
:: Received February 10, 2004
:: Copyright (c) 2004 Association of Mizar Users
deffunc H1( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def1 defines convergent CLVECT_2:def 1 :
theorem Th1: :: CLVECT_2:1
theorem Th2: :: CLVECT_2:2
theorem Th3: :: CLVECT_2:3
theorem Th4: :: CLVECT_2:4
theorem Th5: :: CLVECT_2:5
theorem Th6: :: CLVECT_2:6
theorem Th7: :: CLVECT_2:7
theorem Th8: :: CLVECT_2:8
theorem Th9: :: CLVECT_2:9
:: deftheorem Def2 defines lim CLVECT_2:def 2 :
theorem Th10: :: CLVECT_2:10
theorem :: CLVECT_2:11
theorem :: CLVECT_2:12
theorem Th13: :: CLVECT_2:13
theorem Th14: :: CLVECT_2:14
theorem Th15: :: CLVECT_2:15
theorem Th16: :: CLVECT_2:16
theorem Th17: :: CLVECT_2:17
theorem :: CLVECT_2:18
theorem Th19: :: CLVECT_2:19
:: deftheorem Def3 defines ||. CLVECT_2:def 3 :
theorem Th20: :: CLVECT_2:20
theorem Th21: :: CLVECT_2:21
theorem Th22: :: CLVECT_2:22
:: deftheorem Def4 defines dist CLVECT_2:def 4 :
theorem Th23: :: CLVECT_2:23
theorem Th24: :: CLVECT_2:24
theorem :: CLVECT_2:25
theorem :: CLVECT_2:26
theorem :: CLVECT_2:27
theorem :: CLVECT_2:28
theorem :: CLVECT_2:29
theorem :: CLVECT_2:30
theorem :: CLVECT_2:31
theorem :: CLVECT_2:32
Lm1:
for X being ComplexUnitarySpace
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: :: CLVECT_2:33
theorem :: CLVECT_2:34
theorem :: CLVECT_2:35
theorem :: CLVECT_2:36
theorem :: CLVECT_2:37
theorem :: CLVECT_2:38
theorem :: CLVECT_2:39
:: deftheorem defines Ball CLVECT_2:def 5 :
:: deftheorem defines cl_Ball CLVECT_2:def 6 :
:: deftheorem defines Sphere CLVECT_2:def 7 :
theorem Th40: :: CLVECT_2:40
theorem Th41: :: CLVECT_2:41
theorem :: CLVECT_2:42
theorem :: CLVECT_2:43
theorem :: CLVECT_2:44
theorem :: CLVECT_2:45
theorem :: CLVECT_2:46
theorem Th47: :: CLVECT_2:47
theorem Th48: :: CLVECT_2:48
theorem :: CLVECT_2:49
theorem Th50: :: CLVECT_2:50
theorem Th51: :: CLVECT_2:51
theorem :: CLVECT_2:52
theorem :: CLVECT_2:53
theorem Th54: :: CLVECT_2:54
theorem Th55: :: CLVECT_2:55
theorem :: CLVECT_2:56
deffunc H2( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def8 defines Cauchy CLVECT_2:def 8 :
theorem :: CLVECT_2:57
theorem :: CLVECT_2:58
theorem :: CLVECT_2:59
theorem :: CLVECT_2:60
theorem Th61: :: CLVECT_2:61
theorem :: CLVECT_2:62
theorem Th63: :: CLVECT_2:63
theorem :: CLVECT_2:64
theorem :: CLVECT_2:65
:: deftheorem Def9 defines is_compared_to CLVECT_2:def 9 :
theorem Th66: :: CLVECT_2:66
theorem Th67: :: CLVECT_2:67
theorem :: CLVECT_2:68
theorem :: CLVECT_2:69
theorem :: CLVECT_2:70
theorem :: CLVECT_2:71
theorem :: CLVECT_2:72
theorem :: CLVECT_2:73
:: deftheorem Def10 defines bounded CLVECT_2:def 10 :
theorem Th74: :: CLVECT_2:74
theorem Th75: :: CLVECT_2:75
theorem :: CLVECT_2:76
theorem :: CLVECT_2:77
theorem :: CLVECT_2:78
theorem Th79: :: CLVECT_2:79
theorem Th80: :: CLVECT_2:80
theorem :: CLVECT_2:81
theorem :: CLVECT_2:82
canceled;
theorem :: CLVECT_2:83
canceled;
theorem :: CLVECT_2:84
canceled;
theorem :: CLVECT_2:85
canceled;
theorem :: CLVECT_2:86
canceled;
theorem Th87: :: CLVECT_2:87
theorem Th88: :: CLVECT_2:88
theorem Th89: :: CLVECT_2:89
theorem Th90: :: CLVECT_2:90
theorem :: CLVECT_2:91
canceled;
theorem :: CLVECT_2:92
canceled;
theorem :: CLVECT_2:93
canceled;
theorem Th94: :: CLVECT_2:94
theorem Th95: :: CLVECT_2:95
theorem :: CLVECT_2:96
theorem :: CLVECT_2:97
theorem :: CLVECT_2:98
canceled;
theorem :: CLVECT_2:99
canceled;
theorem :: CLVECT_2:100
theorem :: CLVECT_2:101
theorem :: CLVECT_2:102
theorem :: CLVECT_2:103
theorem :: CLVECT_2:104
theorem :: CLVECT_2:105
theorem :: CLVECT_2:106
:: deftheorem CLVECT_2:def 11 :
canceled;
:: deftheorem Def12 defines complete CLVECT_2:def 12 :
theorem :: CLVECT_2:107
:: deftheorem defines Hilbert CLVECT_2:def 13 :