tsub_add_tsub_comm — Mathlib

English

If b ≤ a and d ≤ c, then a − b + (c − d) = a + c − (b + d).

Русский

Если b ≤ a и d ≤ c, то a − b + (c − d) = a + c − (b + d).

LaTeX

$$$ AddLECancellable\, b \\Rightarrow AddLECancellable\, d \\Rightarrow b ≤ a \\Rightarrow d ≤ c \\Rightarrow (a - b) + (c - d) = a + c - (b + d) $$$

Lean4

protected theorem tsub_add_tsub_comm (hb : AddLECancellable b) (hd : AddLECancellable d) (hba : b ≤ a) (hdc : d ≤ c) :
    a - b + (c - d) = a + c - (b + d) := by
  rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]

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