Definition df-hcau 11312

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

Assertion

Ref	Expression
df-hcau	|- Cauchy = {f | (f:NN-->~H /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)))}

Distinct variable group:   x,y,z,w,f

Detailed syntax breakdown of Definition df-hcau

Step	Hyp	Ref	Expression
1		ccau 11265	. 2 class Cauchy
2		cn 6992	. . . . 5 class NN
3		chil 11258	. . . . 5 class ~H
4		vf	. . . . . 6 set f
5	4	cv 1585	. . . . 5 class f
6	2, 3, 5	wf 4127	. . . 4 wff f:NN-->~H
7		cc0 6752	. . . . . . 7 class 0
8		vx	. . . . . . . 8 set x
9	8	cv 1585	. . . . . . 7 class x
10		clt 6845	. . . . . . 7 class <
11	7, 9, 10	wbr 3507	. . . . . 6 wff 0 < x
12		vy	. . . . . . . . . . . . 13 set y
13	12	cv 1585	. . . . . . . . . . . 12 class y
14		vz	. . . . . . . . . . . . 13 set z
15	14	cv 1585	. . . . . . . . . . . 12 class z
16		cle 6841	. . . . . . . . . . . 12 class <_
17	13, 15, 16	wbr 3507	. . . . . . . . . . 11 wff y <_ z
18		vw	. . . . . . . . . . . . 13 set w
19	18	cv 1585	. . . . . . . . . . . 12 class w
20	13, 19, 16	wbr 3507	. . . . . . . . . . 11 wff y <_ w
21	17, 20	wa 337	. . . . . . . . . 10 wff (y <_ z /\ y <_ w)
22	15, 5	cfv 4131	. . . . . . . . . . . . 13 class (f` z)
23	19, 5	cfv 4131	. . . . . . . . . . . . 13 class (f` w)
24		cmv 11262	. . . . . . . . . . . . 13 class -h
25	22, 23, 24	co 4981	. . . . . . . . . . . 12 class ((f` z) -h (f` w))
26		cno 11264	. . . . . . . . . . . 12 class normh
27	25, 26	cfv 4131	. . . . . . . . . . 11 class (normh` ((f` z) -h (f` w)))
28	27, 9, 10	wbr 3507	. . . . . . . . . 10 wff (normh` ((f` z) -h (f` w))) < x
29	21, 28	wi 3	. . . . . . . . 9 wff ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)
30	29, 18, 2	wral 2355	. . . . . . . 8 wff A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)
31	30, 14, 2	wral 2355	. . . . . . 7 wff A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)
32	31, 12, 2	wrex 2356	. . . . . 6 wff E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)
33	11, 32	wi 3	. . . . 5 wff (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x))
34		cr 6751	. . . . 5 class RR
35	33, 8, 34	wral 2355	. . . 4 wff A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x))
36	6, 35	wa 337	. . 3 wff (f:NN-->~H /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)))
37	36, 4	cab 2128	. 2 class {f | (f:NN-->~H /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)))}
38	1, 37	wceq 1586	1 wff Cauchy = {f | (f:NN-->~H /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)))}

This definition is referenced by:  h2hcau 11319  hcau 11520

Copyright terms: Public domain