eq_tsub_of_add_eq' — Mathlib

English

If b is cancellable and a + c = b, then a = b − c.

Русский

Если b является отменяемым и a + c = b, тогда a = b − c.

LaTeX

$$$ AddLECancellable(b) \land a + c = b \Rightarrow a = b - c $$$

Lean4

/-- Weaker version of `AddLECancellable.eq_tsub_of_add_eq` assuming that `b = a + c` itself is
cancellable rather than `c`. -/
protected theorem eq_tsub_of_add_eq' [AddLeftMono α] (hb : AddLECancellable b) (h : a + c = b) : a = b - c :=
  (hb.tsub_eq_of_eq_add' h.symm).symm

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