add_sub_cancel_right

Mathlib.Data.ENNReal.Operations

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

English

For any a,b ∈ ENNReal with b ≠ ∞, a + b − b = a.

Русский

Для любых a,b ∈ ENNReal, если b ≠ ∞, то a + b − b = a.

LaTeX

$$$$ a + b - b = a. $$$$

Lean4

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

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

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

Разделы

Аффилиация

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