Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hlim Structured version   Unicode version

Definition df-hlim 22477
 Description: Define the limit relation for Hilbert space. See hlimi 22692 for its relational expression. Note that is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-hlim
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-hlim
StepHypRef Expression
1 chli 22432 . 2
2 cn 10002 . . . . . 6
3 chil 22424 . . . . . 6
4 vf . . . . . . 7
54cv 1652 . . . . . 6
62, 3, 5wf 5452 . . . . 5
7 vw . . . . . . 7
87cv 1652 . . . . . 6
98, 3wcel 1726 . . . . 5
106, 9wa 360 . . . 4
11 vz . . . . . . . . . . . 12
1211cv 1652 . . . . . . . . . . 11
1312, 5cfv 5456 . . . . . . . . . 10
14 cmv 22430 . . . . . . . . . 10
1513, 8, 14co 6083 . . . . . . . . 9
16 cno 22428 . . . . . . . . 9
1715, 16cfv 5456 . . . . . . . 8
18 vx . . . . . . . . 9
1918cv 1652 . . . . . . . 8
20 clt 9122 . . . . . . . 8
2117, 19, 20wbr 4214 . . . . . . 7
22 vy . . . . . . . . 9
2322cv 1652 . . . . . . . 8
24 cuz 10490 . . . . . . . 8
2523, 24cfv 5456 . . . . . . 7
2621, 11, 25wral 2707 . . . . . 6
2726, 22, 2wrex 2708 . . . . 5
28 crp 10614 . . . . 5
2927, 18, 28wral 2707 . . . 4
3010, 29wa 360 . . 3
3130, 4, 7copab 4267 . 2
321, 31wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  h2hlm  22485  hlimi  22692
 Copyright terms: Public domain W3C validator