tsub_inj_right — Mathlib

English

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

Русский

Если a − b канцелируемо и b ≤ a, c ≤ a, и a − b = a − c, то b = c.

LaTeX

$$$ \forall a,b,c \in \alpha,\; AddLECancellable(a - b) \land b \le a \land c \le a \land a - b = a - c \Rightarrow b = c $$$

Lean4

protected theorem tsub_inj_right (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) :
    b = c := by
  rw [← hab.inj]
  rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]

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