nullSubmodule_le_ker_toDualMap_right

English

For each x, the null-subspace is contained in the kernel of the right action of the dual map.

Русский

Для каждого x нулевое подпространство содержится в ядре правого действия двойственного отображения.

LaTeX

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

Lean4

/-- For each `x : E`, the kernel of `⟪x, ⬝⟫` includes the null space. -/
theorem nullSubmodule_le_ker_toDualMap_right (x : E) : nullSubmodule 𝕜 E ≤ ker (toDualMap 𝕜 E x) := fun _ hx ↦
  inner_eq_zero_of_right x ((mem_nullSubmodule_iff).mp hx)

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