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

Definition df-nlfn 22442
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 21548 . 2  class  null
2 vt . . 3  set  t
3 cc 8751 . . . 4  class  CC
4 chil 21515 . . . 4  class  ~H
5 cmap 6788 . . . 4  class  ^m
63, 4, 5co 5874 . . 3  class  ( CC 
^m  ~H )
72cv 1631 . . . . 5  class  t
87ccnv 4704 . . . 4  class  `' t
9 cc0 8753 . . . . 5  class  0
109csn 3653 . . . 4  class  { 0 }
118, 10cima 4708 . . 3  class  ( `' t " { 0 } )
122, 6, 11cmpt 4093 . 2  class  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
131, 12wceq 1632 1  wff  null  =  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
Colors of variables: wff set class
This definition is referenced by:  nlfnval  22477
  Copyright terms: Public domain W3C validator