instIsOrderedAddMonoid — Mathlib

English

The Lp space is an ordered additive monoid: addition preserves the order on the left, i.e., for any f ≤ g in Lp and any h, h + f ≤ h + g.

Русский

Пространство Lp является упорядоченным аддитивным моноидом: сложение слева сохраняет порядок, т.д.

LaTeX

$$$\text{IsOrderedAddMonoid}(\,Lp(E,p,\mu)\,).$$$

Lean4

instance instIsOrderedAddMonoid : IsOrderedAddMonoid (Lp E p μ) :=
  { add_le_add_left := fun _ _ => add_le_add_left }

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