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

Definition df-hlim 21548
Description: Define the limit relation for Hilbert space. See hlimi 21763 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 21503 . 2  class  ~~>v
2 cn 9742 . . . . . 6  class  NN
3 chil 21495 . . . . . 6  class  ~H
4 vf . . . . . . 7  set  f
54cv 1622 . . . . . 6  class  f
62, 3, 5wf 5217 . . . . 5  wff  f : NN --> ~H
7 vw . . . . . . 7  set  w
87cv 1622 . . . . . 6  class  w
98, 3wcel 1685 . . . . 5  wff  w  e. 
~H
106, 9wa 358 . . . 4  wff  ( f : NN --> ~H  /\  w  e.  ~H )
11 vz . . . . . . . . . . . 12  set  z
1211cv 1622 . . . . . . . . . . 11  class  z
1312, 5cfv 5221 . . . . . . . . . 10  class  ( f `
 z )
14 cmv 21501 . . . . . . . . . 10  class  -h
1513, 8, 14co 5820 . . . . . . . . 9  class  ( ( f `  z )  -h  w )
16 cno 21499 . . . . . . . . 9  class  normh
1715, 16cfv 5221 . . . . . . . 8  class  ( normh `  ( ( f `  z )  -h  w
) )
18 vx . . . . . . . . 9  set  x
1918cv 1622 . . . . . . . 8  class  x
20 clt 8863 . . . . . . . 8  class  <
2117, 19, 20wbr 4024 . . . . . . 7  wff  ( normh `  ( ( f `  z )  -h  w
) )  <  x
22 vy . . . . . . . . 9  set  y
2322cv 1622 . . . . . . . 8  class  y
24 cuz 10226 . . . . . . . 8  class  ZZ>=
2523, 24cfv 5221 . . . . . . 7  class  ( ZZ>= `  y )
2621, 11, 25wral 2544 . . . . . 6  wff  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  z )  -h  w ) )  < 
x
2726, 22, 2wrex 2545 . . . . 5  wff  E. y  e.  NN  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  z )  -h  w ) )  < 
x
28 crp 10350 . . . . 5  class  RR+
2927, 18, 28wral 2544 . . . 4  wff  A. x  e.  RR+  E. y  e.  NN  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  z )  -h  w ) )  < 
x
3010, 29wa 358 . . 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 4077 . 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 1623 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  21556  hlimi  21763
  Copyright terms: Public domain W3C validator