instLoewnerPartialOrder — Mathlib

English

The Loewner partial order on operators is defined by f ≤ g iff g − f is positive.

Русский

Пусть f, g — операторы. Тогда f ≤ g тогда и только тогда, когда g − f положителен.

LaTeX

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

Lean4

/-- The (Loewner) partial order on continuous linear maps on a Hilbert space determined by
`f ≤ g` if and only if `g - f` is a positive linear map (in the sense of
`ContinuousLinearMap.IsPositive`). With this partial order, the continuous linear maps form a
`StarOrderedRing`. -/
instance instLoewnerPartialOrder : PartialOrder (E →L[𝕜] E)
    where
  le f g := (g - f).IsPositive
  le_refl _ := by simp
  le_trans _ _ _ h₁ h₂ := by simpa using h₁.add h₂
  le_antisymm _ _ h₁ h₂ := coe_inj.mp (le_antisymm h₁.toLinearMap h₂.toLinearMap)

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