IsPositive — Mathlib

English

A finite-dimensional linear map is positive if and only if its associated continuous linear map is positive.

Русский

Положительность линейного отображения в конечномерном случае эквивалентна положительности соответствующего непрерывного линейного отображения.

LaTeX

$$$$T \text{ IsPositive } \iff T^{\text{toContinuousLinearMap}} \text{ IsPositive}$$$$

Lean4

/-- A continuous linear endomorphism `T` of a Hilbert space is **positive** if it is self adjoint
  and `∀ x, 0 ≤ re ⟪T x, x⟫`. -/
def IsPositive (T : E →L[𝕜] E) : Prop :=
  IsSelfAdjoint T ∧ ∀ x, 0 ≤ T.reApplyInnerSelf x

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