tsub_lt_tsub_iff_left_of_le — Mathlib

English

If ha and hb provide AddLECancellable for a and b, and h is b ≤ a, then a − b < a − c iff c < b.

Русский

Если для a и b есть левое седерживание, и b ≤ a, тогда a − b < a − c эквивално c < b.

LaTeX

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

Lean4

/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
protected theorem tsub_lt_tsub_iff_left_of_le (ha : AddLECancellable a) (hb : AddLECancellable b) (h : b ≤ a) :
    a - b < a - c ↔ c < b :=
  lt_iff_lt_of_le_iff_le <| ha.tsub_le_tsub_iff_left hb h

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