isPositive_iff_isSelfAdjoint — Mathlib

English

Let p be an idempotent continuous linear map on E. Then p is positive if and only if p is self-adjoint.

Русский

Пусть p — идемпотентное непрерывное линейное отображение E. Тогда p положительно тогда и только тогда, когда оно самопряжено.

LaTeX

$$$p.IsPositive \;\iff\; IsSelfAdjoint(p)$ (for $p$ idempotent)$$

Lean4

/-- An idempotent operator is positive if and only if it is self-adjoint. -/
@[grind →]
theorem isPositive_iff_isSelfAdjoint {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : p.IsPositive ↔ IsSelfAdjoint p :=
  by
  rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap]
  exact isSelfAdjoint_iff_isSymmetric.symm

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