nonneg_iff_isPositive — Mathlib

English

For a fixed continuous linear operator f on E, 0 ≤ f in the operator order iff f is positive (i.e., f is self-adjoint and nonnegative on the inner product).

Русский

Для фиксированного непрерывного линейного отображения f на E условие 0 ≤ f в порядке операторов эквивалентно тому, что f положительно в смысле операторов (самосопряжён и неотрицателен по скалярному произведению).

LaTeX

$$$0 \le f \iff f \\text{ is positive semidefinite}$$$

Lean4

theorem nonneg_iff_isPositive (f : E →L[𝕜] E) : 0 ≤ f ↔ f.IsPositive := by simpa using le_def 0 f

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