Definition df-hcau 22429

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 22639 for its membership relation. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-hcau	|- Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }

Distinct variable group:   x, y, z, f

Detailed syntax breakdown of Definition df-hcau

Step	Hyp	Ref	Expression
1		ccau 22382	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 set y
3	2	cv 1648	. . . . . . . . . 10 class y
4		vf	. . . . . . . . . . 11 set f
5	4	cv 1648	. . . . . . . . . 10 class f
6	3, 5	cfv 5413	. . . . . . . . 9 class ( f ` y )
7		vz	. . . . . . . . . . 11 set z
8	7	cv 1648	. . . . . . . . . 10 class z
9	8, 5	cfv 5413	. . . . . . . . 9 class ( f ` z )
10		cmv 22381	. . . . . . . . 9 class -h
11	6, 9, 10	co 6040	. . . . . . . 8 class ( ( f ` y ) -h ( f ` z ) )
12		cno 22379	. . . . . . . 8 class normh
13	11, 12	cfv 5413	. . . . . . 7 class ( normh ` ( ( f ` y ) -h ( f ` z ) ) )
14		vx	. . . . . . . 8 set x
15	14	cv 1648	. . . . . . 7 class x
16		clt 9076	. . . . . . 7 class <
17	13, 15, 16	wbr 4172	. . . . . 6 wff ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
18		cuz 10444	. . . . . . 7 class ZZ>=
19	3, 18	cfv 5413	. . . . . 6 class ( ZZ>= ` y )
20	17, 7, 19	wral 2666	. . . . 5 wff A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
21		cn 9956	. . . . 5 class NN
22	20, 2, 21	wrex 2667	. . . 4 wff E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
23		crp 10568	. . . 4 class RR+
24	22, 14, 23	wral 2666	. . 3 wff A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
25		chil 22375	. . . 4 class ~H
26		cmap 6977	. . . 4 class ^m
27	25, 21, 26	co 6040	. . 3 class ( ~H ^m NN )
28	24, 4, 27	crab 2670	. 2 class { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }
29	1, 28	wceq 1649	1 wff Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }

This definition is referenced by:  h2hcau  22435  hcau  22639