le_of_add_le_add_right

Mathlib.Data.ENNReal.Operations

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

English

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

Русский

Пусть a ∈ ENNReal, a ≠ ∞. Если b + a ≤ c + a, то b ≤ c.

LaTeX

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

Lean4

protected theorem le_of_add_le_add_right : a ≠ ∞ → b + a ≤ c + a → b ≤ c :=
  WithTop.le_of_add_le_add_right

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

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

Разделы

Аффилиация

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