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

Definition df-nlfn 27871
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 = (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ (𝑡 “ {0}))

Detailed syntax breakdown of Definition df-nlfn
StepHypRef Expression
1 cnl 26975 . 2 class null
2 vt . . 3 setvar 𝑡
3 cc 9693 . . . 4 class
4 chil 26942 . . . 4 class
5 cmap 7624 . . . 4 class 𝑚
63, 4, 5co 6431 . . 3 class (ℂ ↑𝑚 ℋ)
72cv 1473 . . . . 5 class 𝑡
87ccnv 4931 . . . 4 class 𝑡
9 cc0 9695 . . . . 5 class 0
109csn 4028 . . . 4 class {0}
118, 10cima 4935 . . 3 class (𝑡 “ {0})
122, 6, 11cmpt 4541 . 2 class (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ (𝑡 “ {0}))
131, 12wceq 1474 1 wff null = (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ (𝑡 “ {0}))
Colors of variables: wff setvar class
This definition is referenced by:  nlfnval  27906
  Copyright terms: Public domain W3C validator