add_lt_add_right

Mathlib.Data.ENNReal.Operations

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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