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

Definition df-nlfn 22426
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 21532 . 2  class  null
2 vt . . 3  set  t
3 cc 8735 . . . 4  class  CC
4 chil 21499 . . . 4  class  ~H
5 cmap 6772 . . . 4  class  ^m
63, 4, 5co 5858 . . 3  class  ( CC 
^m  ~H )
72cv 1622 . . . . 5  class  t
87ccnv 4688 . . . 4  class  `' t
9 cc0 8737 . . . . 5  class  0
109csn 3640 . . . 4  class  { 0 }
118, 10cima 4692 . . 3  class  ( `' t " { 0 } )
122, 6, 11cmpt 4077 . 2  class  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
131, 12wceq 1623 1  wff  null  =  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
Colors of variables: wff set class
This definition is referenced by:  nlfnval  22461
  Copyright terms: Public domain W3C validator