lt_add_of_sub_lt_right

Mathlib.Data.ENNReal.Operations

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

English

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

Русский

Если a ≠ ∞ и c ≠ ∞, и a − c < b, то a < b + c.

LaTeX

$$$$ (a \neq \infty) \land (c \neq \infty) \Rightarrow (a - c < b) \Rightarrow a < b + c. $$$$

Lean4

protected theorem lt_add_of_sub_lt_right (h : a ≠ ∞ ∨ c ≠ ∞) : a - c < b → a < b + c :=
  add_comm c b ▸ ENNReal.lt_add_of_sub_lt_left h

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

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

Разделы

Аффилиация

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