add_lt_add_left

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.add_lt_add_left

English

If a ≠ ∞ and b < c, then a + b < a + c.

Русский

Если a ≠ ∞ и b < c, тогда a + b < a + c.

LaTeX

$$a ≠ ∞ → b < c → a + b < a + c$$

Lean4

@[gcongr]
protected theorem add_lt_add_left : a ≠ ∞ → b < c → a + b < a + c :=
  WithTop.add_lt_add_left

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

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

Разделы

Аффилиация

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