of_isSymmetricProjection — Mathlib

English

The same relation between matrix PSD and operator positive holds under basis changes.

Русский

Та же самая связь между PSD матрицы и положительностью оператора сохраняется при смене базиса.

LaTeX

$$$$A \text{PosSemidef} \iff A \text{IsPositive}$$$$

Lean4

/-- A symmetric projection is positive. -/
@[aesop 10% apply, grind →]
theorem of_isSymmetricProjection {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : p.IsPositive :=
  hp.isIdempotentElem.isPositive_iff_isSymmetric.mpr hp.isSymmetric

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