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

Definition df-hcau 21478
Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 21688 for its membership relation. Note that  f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-hcau  |-  Cauchy  =  {
f  e.  ( ~H 
^m  NN )  | 
A. x  e.  RR+  E. y  e.  NN  A. z  e.  ( ZZ>= `  y ) ( normh `  ( ( f `  y )  -h  (
f `  z )
) )  <  x }
Distinct variable group:    x, y, z, f

Detailed syntax breakdown of Definition df-hcau
StepHypRef Expression
1 ccau 21431 . 2  class  Cauchy
2 vy . . . . . . . . . . 11  set  y
32cv 1618 . . . . . . . . . 10  class  y
4 vf . . . . . . . . . . 11  set  f
54cv 1618 . . . . . . . . . 10  class  f
63, 5cfv 4638 . . . . . . . . 9  class  ( f `
 y )
7 vz . . . . . . . . . . 11  set  z
87cv 1618 . . . . . . . . . 10  class  z
98, 5cfv 4638 . . . . . . . . 9  class  ( f `
 z )
10 cmv 21430 . . . . . . . . 9  class  -h
116, 9, 10co 5757 . . . . . . . 8  class  ( ( f `  y )  -h  ( f `  z ) )
12 cno 21428 . . . . . . . 8  class  normh
1311, 12cfv 4638 . . . . . . 7  class  ( normh `  ( ( f `  y )  -h  (
f `  z )
) )
14 vx . . . . . . . 8  set  x
1514cv 1618 . . . . . . 7  class  x
16 clt 8800 . . . . . . 7  class  <
1713, 15, 16wbr 3963 . . . . . 6  wff  ( normh `  ( ( f `  y )  -h  (
f `  z )
) )  <  x
18 cuz 10162 . . . . . . 7  class  ZZ>=
193, 18cfv 4638 . . . . . 6  class  ( ZZ>= `  y )
2017, 7, 19wral 2516 . . . . 5  wff  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  y )  -h  ( f `  z
) ) )  < 
x
21 cn 9679 . . . . 5  class  NN
2220, 2, 21wrex 2517 . . . 4  wff  E. y  e.  NN  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  y )  -h  ( f `  z
) ) )  < 
x
23 crp 10286 . . . 4  class  RR+
2422, 14, 23wral 2516 . . 3  wff  A. x  e.  RR+  E. y  e.  NN  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  y )  -h  ( f `  z
) ) )  < 
x
25 chil 21424 . . . 4  class  ~H
26 cmap 6705 . . . 4  class  ^m
2725, 21, 26co 5757 . . 3  class  ( ~H 
^m  NN )
2824, 4, 27crab 2519 . 2  class  { f  e.  ( ~H  ^m  NN )  |  A. x  e.  RR+  E. y  e.  NN  A. z  e.  ( ZZ>= `  y )
( normh `  ( (
f `  y )  -h  ( f `  z
) ) )  < 
x }
291, 28wceq 1619 1  wff  Cauchy  =  {
f  e.  ( ~H 
^m  NN )  | 
A. x  e.  RR+  E. y  e.  NN  A. z  e.  ( ZZ>= `  y ) ( normh `  ( ( f `  y )  -h  (
f `  z )
) )  <  x }
Colors of variables: wff set class
This definition is referenced by:  h2hcau  21484  hcau  21688
  Copyright terms: Public domain W3C validator