Definition df-hcau

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 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.)

	Ref	Expression
Assertion	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 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccauold	|- Cauchy
1		vf	|- f
2		chba	|- ~H
3		cmap	|- ^m
4		cn	|- NN
5	2 4 3	co	|- ( ~H ^m NN )
6		vx	|- x
7		crp	|- RR+
8		vy	|- y
9		vz	|- z
10		cuz	|- ZZ>=
11	8	cv	|- y
12	11 10	cfv	|- ( ZZ>= ` y )
13		cno	|- normh
14	1	cv	|- f
15	11 14	cfv	|- ( f ` y )
16		cmv	|- -h
17	9	cv	|- z
18	17 14	cfv	|- ( f ` z )
19	15 18 16	co	|- ( ( f ` y ) -h ( f ` z ) )
20	19 13	cfv	|- ( normh ` ( ( f ` y ) -h ( f ` z ) ) )
21		clt	|- <
22	6	cv	|- x
23	20 22 21	wbr	|- ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
24	23 9 12	wral	|- A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
25	24 8 4	wrex	|- E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
26	25 6 7	wral	|- A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
27	26 1 5	crab	|- { 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 }
28	0 27	wceq	|- 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 }