isSymmetric_iff_isOrtho_range_ker

English

If T is an idempotent linear operator (T^2 = T) on an inner product space, then T is symmetric if and only if the range of T is orthogonal to the kernel of T.

Русский

Если T — идемпотентный линейный оператор (T^2 = T) на пространства с скалярным произведением, то T симметричен тогда и только тогда, когда образ(T) ортогонален ядру(T).

LaTeX

$$$T^2 = T\;\Rightarrow\; (\operatorname{range} T) \perp (\ker T)$ iff $T$ is symmetric$$

Lean4

/-- An idempotent operator is symmetric if and only if its range is
pairwise orthogonal to its kernel. -/
theorem isSymmetric_iff_isOrtho_range_ker {T : E →ₗ[𝕜] E} (hT : IsIdempotentElem T) :
    T.IsSymmetric ↔ (LinearMap.range T) ⟂ (LinearMap.ker T) := by
  rw [← IsCompl.projection_isSymmetric_iff hT.isProj_range.isCompl, ← hT.eq_isCompl_projection]

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