Definition df-hlim 5107

Description: Define the limit relation for Hilbert space. See hlim 5108 for its relational expression. Note that f:NN-->H~ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96.

Assertion

Ref	Expression
df-hlim	|- ~~>v = {<.f, w>. | ((f:NN-->H~ /\ w e. H~) /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x)))}

Distinct variable group(s):   x,y,z,f

Detailed syntax breakdown of Definition df-hlim

Step	Hyp	Ref	Expression
1		chli 4966	. 2 class ~~>v
2		cn 4093	. . . . . 6 class NN
3		chil 4958	. . . . . 6 class H~
4		vf	. . . . . . 7 set f
5	4	cv 1089	. . . . . 6 class f
6	2, 3, 5	wf 2418	. . . . 5 wff f:NN-->H~
7		vw	. . . . . . 7 set w
8	7	cv 1089	. . . . . 6 class w
9	8, 3	wcel 1092	. . . . 5 wff w e. H~
10	6, 9	wa 196	. . . 4 wff (f:NN-->H~ /\ w e. H~)
11		cc0 4028	. . . . . . 7 class 0
12		vx	. . . . . . . 8 set x
13	12	cv 1089	. . . . . . 7 class x
14		clt 4033	. . . . . . 7 class <
15	11, 13, 14	wbr 2054	. . . . . 6 wff 0 < x
16		vy	. . . . . . . . . . 11 set y
17	16	cv 1089	. . . . . . . . . 10 class y
18		vz	. . . . . . . . . . 11 set z
19	18	cv 1089	. . . . . . . . . 10 class z
20		cle 4092	. . . . . . . . . 10 class <_
21	17, 19, 20	wbr 2054	. . . . . . . . 9 wff y <_ z
22	19, 5	cfv 2422	. . . . . . . . . . . 12 class (f` z)
23		cmv 4962	. . . . . . . . . . . 12 class -v
24	22, 8, 23	co 3001	. . . . . . . . . . 11 class ((f` z) -v w)
25		cno 4964	. . . . . . . . . . 11 class norm
26	24, 25	cfv 2422	. . . . . . . . . 10 class (norm` ((f` z) -v w))
27	26, 13, 14	wbr 2054	. . . . . . . . 9 wff (norm` ((f` z) -v w)) < x
28	21, 27	wi 2	. . . . . . . 8 wff (y <_ z -> (norm` ((f` z) -v w)) < x)
29	28, 18, 2	wral 1201	. . . . . . 7 wff A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x)
30	29, 16, 2	wrex 1202	. . . . . 6 wff E.y e. NN A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x)
31	15, 30	wi 2	. . . . 5 wff (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x))
32		cr 4027	. . . . 5 class RR
33	31, 12, 32	wral 1201	. . . 4 wff A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x))
34	10, 33	wa 196	. . 3 wff ((f:NN-->H~ /\ w e. H~) /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x)))
35	34, 4, 7	copab 2055	. 2 class {<.f, w>. | ((f:NN-->H~ /\ w e. H~) /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x)))}
36	1, 35	wceq 1091	1 wff ~~>v = {<.f, w>. | ((f:NN-->H~ /\ w e. H~) /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((f` z) -v w)) < x)))}

This definition is referenced by:  hlim 5108  hlim2 5112

metamath.org