le_tsub_iff_le_tsub — Mathlib

English

Let α be an ordered additive semigroup with subtraction. If a ≤ b and c ≤ b, then a ≤ b − c is equivalent to c ≤ b − a.

Русский

Пусть α имеет упорядоченную аддитивную полугруппу с вычитанием. При a ≤ b и c ≤ b имеем равносильность: a ≤ b − c и c ≤ b − a.

LaTeX

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

Lean4

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

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