add_sub_cancel_left

Mathlib.Data.ENNReal.Operations

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

English

Protected form: If a = b + c with a finite, then a − b = c.

Русский

Защищенная форма: если a = b + c и a конечное, тогда a − b = c.

LaTeX

$$$$ a = b + c \Rightarrow a - b = c \text{ при } a \neq \infty. $$$$

Lean4

protected theorem add_sub_cancel_left (ha : a ≠ ∞) : a + b - a = b := by simp [ha]

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

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

Разделы

Аффилиация

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