tsub_lt_tsub_iff_right — Mathlib

English

Under cancellability assumptions, a − b < a − c is equivalent to c < b when b ≤ a.

Русский

При условиях отменяемости, a − b < a − c эквивалентно c < b если b ≤ a.

LaTeX

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

Lean4

/-- This lemma also holds for `ENNReal`, but we need a different proof for that. -/
theorem tsub_lt_tsub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b :=
  Contravariant.AddLECancellable.tsub_lt_tsub_iff_right h

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