orthogonal_ker — Mathlib

English

The adjoint of the orthogonal projection equals the inclusion map; a variant formulation of the previous fact.

Русский

Сопряжённый ортогональной проекции равен включению; вариант формулировки предыдущего факта.

LaTeX

$$$(U.orthogonalProjection)^{\dagger} = U.subtypeL$$$

Lean4

theorem orthogonal_ker (T : E →L[𝕜] F) : (LinearMap.ker T)ᗮ = (LinearMap.range (T†)).topologicalClosure :=
  by
  rw [← Submodule.orthogonal_orthogonal_eq_closure]
  apply le_antisymm
  all_goals refine Submodule.orthogonal_le fun x hx ↦ ?_
  · refine ext_inner_left 𝕜 fun y ↦ ?_
    simp [← T.adjoint_inner_left, hx _ (LinearMap.mem_range_self (T†) y)]
  · rintro _ ⟨y, rfl⟩
    simp_all [T.adjoint_inner_left]

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