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 ) }