tsub_lt_iff_left — Mathlib

English

Let α be a partially ordered additive commutative semigroup with subtraction defined and left-cancellability for b. If b ≤ a, then a − b < c if and only if a < b + c.

Русский

Пусть α — частично упорядоченная коммутативная полугруппа с определённым вычитанием и левой канцелируемостью для b. При условии b ≤ a верно: a − b < c тогда и только если a < b + c.

LaTeX

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

Lean4

protected theorem tsub_lt_iff_left (hb : AddLECancellable b) (hba : b ≤ a) : a - b < c ↔ a < b + c :=
  by
  refine ⟨hb.lt_add_of_tsub_lt_left, ?_⟩
  intro h; refine (tsub_le_iff_left.mpr h.le).lt_of_ne ?_
  rintro rfl; exact h.ne' (add_tsub_cancel_of_le hba)

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