isIdempotentElem_iff_eq_isCompl_projection_range_ker

English

A linear map is idempotent iff it equals the projection onto its range along its kernel.

Русский

Линейное отображение идемпотентно тогда и только тогда, когда оно равно проекции на образ вдоль ядра.

LaTeX

$$$\IsIdempotentElem T \iff \exists h, T = h.projection$ where $h: IsCompl(\operatorname{range} T, \ker T)$$$

Lean4

/-- A linear map is an idempotent if and only if it equals the projection
onto its range along its kernel. -/
theorem isIdempotentElem_iff_eq_isCompl_projection_range_ker {T : E →ₗ[R] E} :
    IsIdempotentElem T ↔ ∃ (h : IsCompl (range T) (ker T)), T = h.projection :=
  ⟨fun hT => ⟨hT.isProj_range.isCompl, hT.eq_isCompl_projection⟩, fun ⟨hT, h⟩ =>
    h.symm ▸ hT.projection_isIdempotentElem⟩

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