tsub_le_tsub_iff_left — Mathlib

English

For AddLECancellable a and c with c ≤ a, a − b ≤ a − c iff c ≤ b.

Русский

Для AddLECancellable a и c с c ≤ a, выполняется a − b ≤ a − c ⇔ c ≤ b.

LaTeX

$$$$ a - b \le a - c \iff c \le b \quad\text{(when } a,c\text{ are AddLECancellable and } c \le a) $$$$

Lean4

protected theorem tsub_le_tsub_iff_left (ha : AddLECancellable a) (hc : AddLECancellable c) (h : c ≤ a) :
    a - b ≤ a - c ↔ c ≤ b := by
  refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
  rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self), add_comm b]
  apply ha

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