sub_eq_of_eq_add_rev' — Mathlib

English

Weaker version: If a = b + c and b ≠ ∞, then a − b = c.

Русский

Учетная слабая версия: если a = b + c и b ≠ ∞, то a − b = c.

LaTeX

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

Lean4

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

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