orthogonal_range — Mathlib

English

For any symmetric linear map T, the orthogonal complement of its range equals its kernel.

Русский

Для симметричного линейного отображения T ортогональное дополнение образа совпадает с ядром.

LaTeX

$$If $T$ is symmetric, then $\operatorname{range}(T)^{\perp} = \ker(T)$$$

Lean4

theorem orthogonal_range {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) : (LinearMap.range T)ᗮ = LinearMap.ker T :=
  by
  ext x
  constructor
  · simpa [Submodule.mem_orthogonal, hT _ x] using ext_inner_left 𝕜 (x := T x) (y := 0)
  · simp_all [Submodule.mem_orthogonal, hT _ x]

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