le_def

Mathlib.Analysis.InnerProductSpace.Positive

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.le_def

English

A linear operator T is less than or equal to another operator S in the Loewner order if and only if S − T is positive.

Русский

Оператор T не превосходит S по порядку Лёвнера тогда и только тогда, когда S − T положителен.

LaTeX

$$$f \\le g \\iff (g-f) \\text{ IsPositive}. $$$

Lean4

theorem le_def (f g : E →L[𝕜] E) : f ≤ g ↔ (g - f).IsPositive :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru