add_lt_add_iff_right

Mathlib.Data.ENNReal.Operations

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

English

If a ≠ ∞, then (b + a < c + a ↔ b < c).

Русский

Если a ≠ ∞, то (b + a < c + a) эквивалентно (b < c).

LaTeX

$$a ≠ ∞ → (b + a < c + a ↔ b < c)$$

Lean4

protected theorem add_lt_add_iff_right : a ≠ ∞ → (b + a < c + a ↔ b < c) :=
  WithTop.add_lt_add_iff_right

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

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

Разделы

Аффилиация

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