eq_sub_of_add_eq

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

If b = a + c with c ≠ ∞, then a = b − c.

Русский

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

LaTeX

$$$$ b = a + c \land c \neq \infty \;\Rightarrow\; a = b - c. $$$$

Lean4

/-- See `ENNReal.eq_sub_of_add_eq'` for a version assuming that `b = a + c` itself is finite rather
than `c`. -/
protected theorem eq_sub_of_add_eq (hc : c ≠ ∞) : a + c = b → a = b - c :=
  (cancel_of_ne hc).eq_tsub_of_add_eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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