HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hlim Unicode version

Definition df-hlim 21477
Description: Define the limit relation for Hilbert space. See hlimi 21692 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.)
Assertion
Ref Expression
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 ) }
Distinct variable group:    x, y, z, f, w

Detailed syntax breakdown of Definition df-hlim
StepHypRef Expression
1 chli 21432 . 2  class  ~~>v
2 cn 9679 . . . . . 6  class  NN
3 chil 21424 . . . . . 6  class  ~H
4 vf . . . . . . 7  set  f
54cv 1618 . . . . . 6  class  f
62, 3, 5wf 4634 . . . . 5  wff  f : NN --> ~H
7 vw . . . . . . 7  set  w
87cv 1618 . . . . . 6  class  w
98, 3wcel 1621 . . . . 5  wff  w  e. 
~H
106, 9wa 360 . . . 4  wff  ( f : NN --> ~H  /\  w  e.  ~H )
11 vz . . . . . . . . . . . 12  set  z
1211cv 1618 . . . . . . . . . . 11  class  z
1312, 5cfv 4638 . . . . . . . . . 10  class  ( f `
 z )
14 cmv 21430 . . . . . . . . . 10  class  -h
1513, 8, 14co 5757 . . . . . . . . 9  class  ( ( f `  z )  -h  w )
16 cno 21428 . . . . . . . . 9  class  normh
1715, 16cfv 4638 . . . . . . . 8  class  ( normh `  ( ( f `  z )  -h  w
) )
18 vx . . . . . . . . 9  set  x
1918cv 1618 . . . . . . . 8  class  x
20 clt 8800 . . . . . . . 8  class  <
2117, 19, 20wbr 3963 . . . . . . 7  wff  ( normh `  ( ( f `  z )  -h  w
) )  <  x
22 vy . . . . . . . . 9  set  y
2322cv 1618 . . . . . . . 8  class  y
24 cuz 10162 . . . . . . . 8  class  ZZ>=
2523, 24cfv 4638 . . . . . . 7  class  ( ZZ>= `  y )
2621, 11, 25wral 2516 . . . . . 6  wff  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  z )  -h  w ) )  < 
x
2726, 22, 2wrex 2517 . . . . 5  wff  E. y  e.  NN  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  z )  -h  w ) )  < 
x
28 crp 10286 . . . . 5  class  RR+
2927, 18, 28wral 2516 . . . 4  wff  A. x  e.  RR+  E. y  e.  NN  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  z )  -h  w ) )  < 
x
3010, 29wa 360 . . 3  wff  ( ( 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
)
3130, 4, 7copab 4016 . 2  class  { <. 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
) }
321, 31wceq 1619 1  wff  ~~>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 ) }
Colors of variables: wff set class
This definition is referenced by:  h2hlm  21485  hlimi  21692
  Copyright terms: Public domain W3C validator