nullSubmodule_le_ker_toDualMap_left

English

The kernel of toDualMap contains the left null subspace.

Русский

Ядро toDualMap содержит левое нулевое подпространство.

LaTeX

$$nullSubmodule 𝕜 E ≤ ker (toDualMap 𝕜 E)$$

Lean4

/-- The kernel of the map `x ↦ ⟪·, x⟫` includes the null space. -/
theorem nullSubmodule_le_ker_toDualMap_left : nullSubmodule 𝕜 E ≤ ker (toDualMap 𝕜 E) := fun _ hx ↦
  ContinuousLinearMap.ext <| fun y ↦ inner_eq_zero_of_left y hx

Похожие утверждения