isStarProjection_iff_eq_starProjection_range

English

An idempotent operator is self-adjoint if and only if it is normal.

Русский

Идемпотентный оператор самосопряжён тогда и только тогда, когда он нормален.

LaTeX

$$$\\text{IsIdempotentElem}(T) \\Rightarrow (\\text{IsSelfAdjoint}(T) \\iff \\text{IsStarNormal}(T))$$$

Lean4

/-- An operator is a star projection if and only if it is an orthogonal projection. -/
theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E →L[𝕜] E} :
    IsStarProjection p ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection :=
  by
  simp_rw [← p.isStarProjection_iff_isSymmetricProjection.symm.eq,
    LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, coe_inj]
  rfl

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