tsub_lt_iff_tsub_lt — Mathlib

English

Let α be an ordered additive commutative semigroup equipped with a subtraction operation. If b and c lie below a (i.e., b ≤ a and c ≤ a), then a − b < c is equivalent to a − c < b.

Русский

Пусть α — упорядоченная коммутативная полугруппа с операцией вычитания. Если b и c не превосходят a (b ≤ a и c ≤ a), то a − b < c тогда и только тогда, когда a − c < b.

LaTeX

$$$\forall a,b,c \in \alpha\,\bigl((b \le a) \land (c \le a) \implies (a - b < c \iff a - c < b)\bigr)$$$

Lean4

theorem tsub_lt_iff_tsub_lt (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b :=
  Contravariant.AddLECancellable.tsub_lt_iff_tsub_lt Contravariant.AddLECancellable h₁ h₂

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