lt_tsub_iff_right_of_le — Mathlib

English

In an ordered subtraction setting, if c ≤ b, then a < b − c is equivalent to a + c < b.

Русский

В обстановке упорядоченного вычитания, если c ≤ b, то a < b − c эквивалентно a + c < b.

LaTeX

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

Lean4

/-- See `lt_tsub_iff_right` for a stronger statement in a linear order. -/
theorem lt_tsub_iff_right_of_le (h : c ≤ b) : a < b - c ↔ a + c < b :=
  Contravariant.AddLECancellable.lt_tsub_iff_right_of_le h

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