ext_iff — Mathlib

English

For a bounded operator T, being a star projection is equivalent to being a symmetric projection.

Русский

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

LaTeX

$$$\\text{IsStarProjection}(T) \\iff T.\\IsSymmetricProjection$$$

Lean4

/-- Star projection operators are equal iff their range are. -/
theorem ext_iff {S : E →L[𝕜] E} (hS : IsStarProjection S) (hT : IsStarProjection T) :
    S = T ↔ LinearMap.range S = LinearMap.range T := by
  simpa using
    LinearMap.IsSymmetricProjection.ext_iff (isStarProjection_iff_isSymmetricProjection.mp hS)
      (isStarProjection_iff_isSymmetricProjection.mp hT)

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