eq_isCompl_projection — Mathlib

English

An idempotent operator T equals the projection onto its range along its kernel.

Русский

Идемпотентный оператор T равен проекции на образ вдоль ядра.

LaTeX

$$T = \text{IsCompl.projection} \text{ for } hT$$

Lean4

/-- An idempotent linear operator is equal to the linear projection onto
its range along its kernel. -/
theorem eq_isCompl_projection {T : E →ₗ[R] E} (hT : IsIdempotentElem T) : T = hT.isCompl.projection :=
  by
  convert ofIsCompl_subtype_zero_eq hT.isCompl
  exact ofIsCompl_eq _ (by simp [hT.isProj_range.map_id]) (by simp) |>.symm

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