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 ≠ ∞ and b = a + c, then a = b − c.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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