instIsOrderedAddMonoid — Mathlib

English

Outer measures form an ordered additive monoid: addition is monotone with respect to set inclusion, and the order interacts with addition via the usual inequality.

Русский

Внешние меры образуют упорядченный аддитивный моноид: сумма монотонна по включению и порядок взаимодействует со сложением через обычные неравенства.

LaTeX

$$$\text{IsOrderedAddMonoid }(OuterMeasure\, \alpha).$$$

Lean4

instance instIsOrderedAddMonoid {α : Type*} : IsOrderedAddMonoid (OuterMeasure α) where
  add_le_add_left _ _ h _ s := add_le_add_left (h s) _

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