Metamath Proof Explorer

Definition df-hlim

Description: Define the limit relation for Hilbert space. See hlimi 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. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 chli 
 |-  ~~>v
1 vf 
 |-  f
2 vw 
 |-  w
3 1 cv 
 |-  f
4 cn 
 |-  NN
5 chba 
 |-  ~H
6 4 5 3 wf 
 |-  f : NN --> ~H
7 2 cv 
 |-  w
8 7 5 wcel 
 |-  w e. ~H
9 6 8 wa 
 |-  ( f : NN --> ~H /\ w e. ~H )
10 vx 
 |-  x
11 crp 
 |-  RR+
12 vy 
 |-  y
13 vz 
 |-  z
14 cuz 
 |-  ZZ>=
15 12 cv 
 |-  y
16 15 14 cfv 
 |-  ( ZZ>= ` y )
17 cno 
 |-  normh
18 13 cv 
 |-  z
19 18 3 cfv 
 |-  ( f ` z )
20 cmv 
 |-  -h
21 19 7 20 co 
 |-  ( ( f ` z ) -h w )
22 21 17 cfv 
 |-  ( normh ` ( ( f ` z ) -h w ) )
23 clt 
 |-  <
24 10 cv 
 |-  x
25 22 24 23 wbr 
 |-  ( normh ` ( ( f ` z ) -h w ) ) < x
26 25 13 16 wral 
 |-  A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x
27 26 12 4 wrex 
 |-  E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x
28 27 10 11 wral 
 |-  A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x
29 9 28 wa 
 |-  ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x )
30 29 1 2 copab 
 |-  { <. f , w >. | ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) }
31 0 30 wceq 
 |-  ~~>v = { <. f , w >. | ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) }