tsub_lt_iff_tsub_lt — Mathlib

English

If b and c are left-cancellable and both ≤ a, then a − b < c is equivalent to a − c < b.

Русский

Если b и c слева канцелируемы и оба не превосходят a, тогда a − b < c эквивалично a − c < b.

LaTeX

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

Lean4

protected theorem tsub_lt_iff_tsub_lt (hb : AddLECancellable b) (hc : AddLECancellable c) (h₁ : b ≤ a) (h₂ : c ≤ a) :
    a - b < c ↔ a - c < b := by rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right h₂]

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