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

Definition df-nlfn 26637
Description: Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-nlfn  |-  null  =  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )

Detailed syntax breakdown of Definition df-nlfn
StepHypRef Expression
1 cnl 25741 . 2  class  null
2 vt . . 3  setvar  t
3 cc 9493 . . . 4  class  CC
4 chil 25708 . . . 4  class  ~H
5 cmap 7422 . . . 4  class  ^m
63, 4, 5co 6281 . . 3  class  ( CC 
^m  ~H )
72cv 1382 . . . . 5  class  t
87ccnv 4988 . . . 4  class  `' t
9 cc0 9495 . . . . 5  class  0
109csn 4014 . . . 4  class  { 0 }
118, 10cima 4992 . . 3  class  ( `' t " { 0 } )
122, 6, 11cmpt 4495 . 2  class  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
131, 12wceq 1383 1  wff  null  =  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
Colors of variables: wff setvar class
This definition is referenced by:  nlfnval  26672
  Copyright terms: Public domain W3C validator