tsub_tsub_assoc — Mathlib

English

If hbc is AddLECancellable for (b − c) and h1: b ≤ a, h2: c ≤ b, then a − (b − c) = a − b + c.

Русский

Если hbc — AddLECancellable для (b − c) и b ≤ a, c ≤ b, то a − (b − c) = a − b + c.

LaTeX

$$$ hbc : AddLECancellable (b - c) \\Rightarrow b \\le a \\Rightarrow c \\le b \\Rightarrow a - (b - c) = a - b + c $$$

Lean4

protected theorem tsub_tsub_assoc (hbc : AddLECancellable (b - c)) (h₁ : b ≤ a) (h₂ : c ≤ b) :
    a - (b - c) = a - b + c :=
  hbc.tsub_eq_of_eq_add <| by rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]

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