tsub_eq_of_eq_add — Mathlib

English

If b is cancellable with respect to addition 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

/-- See `AddLECancellable.tsub_eq_of_eq_add'` for a version assuming that `a = c + b` itself is
cancellable rather than `b`. -/
protected theorem tsub_eq_of_eq_add (hb : AddLECancellable b) (h : a = c + b) : a - b = c :=
  le_antisymm (tsub_le_iff_right.mpr h.le) <| by
    rw [h]
    exact hb.le_add_tsub

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