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

Definition df-cnfn 22419
Description: Define the set of continuous functionals on Hilbert space. For every "epsilon" ( y) there is an "delta" ( z) such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-cnfn  |-  ConFn  =  {
t  e.  ( CC 
^m  ~H )  |  A. x  e.  ~H  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  ~H  ( ( normh `  (
w  -h  x ) )  <  z  -> 
( abs `  (
( t `  w
)  -  ( t `
 x ) ) )  <  y ) }
Distinct variable group:    w, t, x, y, z

Detailed syntax breakdown of Definition df-cnfn
StepHypRef Expression
1 ccnfn 21525 . 2  class  ConFn
2 vw . . . . . . . . . . . 12  set  w
32cv 1627 . . . . . . . . . . 11  class  w
4 vx . . . . . . . . . . . 12  set  x
54cv 1627 . . . . . . . . . . 11  class  x
6 cmv 21497 . . . . . . . . . . 11  class  -h
73, 5, 6co 5819 . . . . . . . . . 10  class  ( w  -h  x )
8 cno 21495 . . . . . . . . . 10  class  normh
97, 8cfv 5221 . . . . . . . . 9  class  ( normh `  ( w  -h  x
) )
10 vz . . . . . . . . . 10  set  z
1110cv 1627 . . . . . . . . 9  class  z
12 clt 8862 . . . . . . . . 9  class  <
139, 11, 12wbr 4024 . . . . . . . 8  wff  ( normh `  ( w  -h  x
) )  <  z
14 vt . . . . . . . . . . . . 13  set  t
1514cv 1627 . . . . . . . . . . . 12  class  t
163, 15cfv 5221 . . . . . . . . . . 11  class  ( t `
 w )
175, 15cfv 5221 . . . . . . . . . . 11  class  ( t `
 x )
18 cmin 9032 . . . . . . . . . . 11  class  -
1916, 17, 18co 5819 . . . . . . . . . 10  class  ( ( t `  w )  -  ( t `  x ) )
20 cabs 11713 . . . . . . . . . 10  class  abs
2119, 20cfv 5221 . . . . . . . . 9  class  ( abs `  ( ( t `  w )  -  (
t `  x )
) )
22 vy . . . . . . . . . 10  set  y
2322cv 1627 . . . . . . . . 9  class  y
2421, 23, 12wbr 4024 . . . . . . . 8  wff  ( abs `  ( ( t `  w )  -  (
t `  x )
) )  <  y
2513, 24wi 6 . . . . . . 7  wff  ( (
normh `  ( w  -h  x ) )  < 
z  ->  ( abs `  ( ( t `  w )  -  (
t `  x )
) )  <  y
)
26 chil 21491 . . . . . . 7  class  ~H
2725, 2, 26wral 2544 . . . . . 6  wff  A. w  e.  ~H  ( ( normh `  ( w  -h  x
) )  <  z  ->  ( abs `  (
( t `  w
)  -  ( t `
 x ) ) )  <  y )
28 crp 10349 . . . . . 6  class  RR+
2927, 10, 28wrex 2545 . . . . 5  wff  E. z  e.  RR+  A. w  e. 
~H  ( ( normh `  ( w  -h  x
) )  <  z  ->  ( abs `  (
( t `  w
)  -  ( t `
 x ) ) )  <  y )
3029, 22, 28wral 2544 . . . 4  wff  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  ~H  ( ( normh `  (
w  -h  x ) )  <  z  -> 
( abs `  (
( t `  w
)  -  ( t `
 x ) ) )  <  y )
3130, 4, 26wral 2544 . . 3  wff  A. x  e.  ~H  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  ~H  (
( normh `  ( w  -h  x ) )  < 
z  ->  ( abs `  ( ( t `  w )  -  (
t `  x )
) )  <  y
)
32 cc 8730 . . . 4  class  CC
33 cmap 6767 . . . 4  class  ^m
3432, 26, 33co 5819 . . 3  class  ( CC 
^m  ~H )
3531, 14, 34crab 2548 . 2  class  { t  e.  ( CC  ^m  ~H )  |  A. x  e.  ~H  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  ~H  ( ( normh `  (
w  -h  x ) )  <  z  -> 
( abs `  (
( t `  w
)  -  ( t `
 x ) ) )  <  y ) }
361, 35wceq 1628 1  wff  ConFn  =  {
t  e.  ( CC 
^m  ~H )  |  A. x  e.  ~H  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  ~H  ( ( normh `  (
w  -h  x ) )  <  z  -> 
( abs `  (
( t `  w
)  -  ( t `
 x ) ) )  <  y ) }
Colors of variables: wff set class
This definition is referenced by:  elcnfn  22454  hhcnf  22477
  Copyright terms: Public domain W3C validator