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

Definition df-nlfn 22351
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 21457 . 2  class  null
2 vt . . 3  set  t
3 cc 8668 . . . 4  class  CC
4 chil 21424 . . . 4  class  ~H
5 cmap 6705 . . . 4  class  ^m
63, 4, 5co 5757 . . 3  class  ( CC 
^m  ~H )
72cv 1618 . . . . 5  class  t
87ccnv 4625 . . . 4  class  `' t
9 cc0 8670 . . . . 5  class  0
109csn 3581 . . . 4  class  { 0 }
118, 10cima 4629 . . 3  class  ( `' t " { 0 } )
122, 6, 11cmpt 4017 . 2  class  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
131, 12wceq 1619 1  wff  null  =  ( t  e.  ( CC  ^m  ~H )  |->  ( `' t " { 0 } ) )
Colors of variables: wff set class
This definition is referenced by:  nlfnval  22386
  Copyright terms: Public domain W3C validator