tsub_le_tsub_iff_left — Mathlib

English

For AddLeftReflectLE α, tsub_le_tsub_iff_left holds: a − b ≤ a − c iff c ≤ b (under appropriate hypotheses).

Русский

При AddLeftReflectLE α выполняется тождество tsub_le_tsub_iff_left: a − b ≤ a − c ⇔ c ≤ b (при нужных гипотезах).

LaTeX

$$$$ a - b \le a - c \iff c \le b $$$$

Lean4

theorem tsub_le_tsub_iff_left (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b :=
  Contravariant.AddLECancellable.tsub_le_tsub_iff_left Contravariant.AddLECancellable h

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