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

Definition df-hlim 21382
 Description: Define the limit relation for Hilbert space. See hlimi 21597 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 21337 . 2
2 cn 9626 . . . . . 6
3 chil 21329 . . . . . 6
4 vf . . . . . . 7
54cv 1618 . . . . . 6
62, 3, 5wf 4588 . . . . 5
7 vw . . . . . . 7
87cv 1618 . . . . . 6
98, 3wcel 1621 . . . . 5
106, 9wa 360 . . . 4
11 vz . . . . . . . . . . . 12
1211cv 1618 . . . . . . . . . . 11
1312, 5cfv 4592 . . . . . . . . . 10
14 cmv 21335 . . . . . . . . . 10
1513, 8, 14co 5710 . . . . . . . . 9
16 cno 21333 . . . . . . . . 9
1715, 16cfv 4592 . . . . . . . 8
18 vx . . . . . . . . 9
1918cv 1618 . . . . . . . 8
20 clt 8747 . . . . . . . 8
2117, 19, 20wbr 3920 . . . . . . 7
22 vy . . . . . . . . 9
2322cv 1618 . . . . . . . 8
24 cuz 10109 . . . . . . . 8
2523, 24cfv 4592 . . . . . . 7
2621, 11, 25wral 2509 . . . . . 6
2726, 22, 2wrex 2510 . . . . 5
28 crp 10233 . . . . 5
2927, 18, 28wral 2509 . . . 4
3010, 29wa 360 . . 3
3130, 4, 7copab 3973 . 2
321, 31wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  h2hlm  21390  hlimi  21597
 Copyright terms: Public domain W3C validator