tsub_right_inj — Mathlib

English

If a,b,c are AddLECancellable and b ≤ a, c ≤ a, then a − b = a − c iff b = c.

Русский

Если a,b,c — AddLECancellable и b ≤ a, c ≤ a, тогда a − b = a − c ⇔ b = c.

LaTeX

$$$$ a - b = a - c \iff b = c \text{ whenever } b \le a, c \le a $$$$

Lean4

protected theorem tsub_right_inj (ha : AddLECancellable a) (hb : AddLECancellable b) (hc : AddLECancellable c)
    (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c := by
  simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca, and_comm]

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