instIsOrderedAddMonoid

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.instIsOrderedAddMonoid

English

If μ ≤ ν then μ ≤ ν' + ν for any ν'.

Русский

Если μ ≤ ν, то для любого ν' выполняется μ ≤ ν' + ν.

LaTeX

$$$ \\text{If } μ \\le ν \\text{ then } μ \\le ν' + ν \\text{ for all } ν' $$$

Lean4

instance instIsOrderedAddMonoid {_ : MeasurableSpace α} : IsOrderedAddMonoid (Measure α) where
  add_le_add_left _ _ h _ s := add_le_add_left (h s) _

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

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

Разделы

Аффилиация

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