Home Hilbert Space Explorer < Previous   Next > Related theorems Unicode version

Definition df-hcau 11312
 Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 11520 for its membership relation. Note that is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96.
Assertion
Ref Expression
df-hcau
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-hcau
StepHypRef Expression
1 ccau 11265 . 2
2 cn 6992 . . . . 5
3 chil 11258 . . . . 5
4 vf . . . . . 6
54cv 1585 . . . . 5
62, 3, 5wf 4127 . . . 4
7 cc0 6752 . . . . . . 7
8 vx . . . . . . . 8
98cv 1585 . . . . . . 7
10 clt 6845 . . . . . . 7
117, 9, 10wbr 3507 . . . . . 6
12 vy . . . . . . . . . . . . 13
1312cv 1585 . . . . . . . . . . . 12
14 vz . . . . . . . . . . . . 13
1514cv 1585 . . . . . . . . . . . 12
16 cle 6841 . . . . . . . . . . . 12
1713, 15, 16wbr 3507 . . . . . . . . . . 11
18 vw . . . . . . . . . . . . 13
1918cv 1585 . . . . . . . . . . . 12
2013, 19, 16wbr 3507 . . . . . . . . . . 11
2117, 20wa 337 . . . . . . . . . 10
2215, 5cfv 4131 . . . . . . . . . . . . 13
2319, 5cfv 4131 . . . . . . . . . . . . 13
24 cmv 11262 . . . . . . . . . . . . 13
2522, 23, 24co 4981 . . . . . . . . . . . 12
26 cno 11264 . . . . . . . . . . . 12
2725, 26cfv 4131 . . . . . . . . . . 11
2827, 9, 10wbr 3507 . . . . . . . . . 10
2921, 28wi 3 . . . . . . . . 9
3029, 18, 2wral 2355 . . . . . . . 8
3130, 14, 2wral 2355 . . . . . . 7
3231, 12, 2wrex 2356 . . . . . 6
3311, 32wi 3 . . . . 5
34 cr 6751 . . . . 5
3533, 8, 34wral 2355 . . . 4
366, 35wa 337 . . 3
3736, 4cab 2128 . 2
381, 37wceq 1586 1
 Colors of variables: wff set class This definition is referenced by:  h2hcau 11319  hcau 11520