tsub_lt_tsub_iff_right — Mathlib

English

If c ≤ a and c is left cancellable, then a − c < b − c if and only if a < b.

Русский

Если c ≤ a и c удовлетворяет условию левой отмены, то a − c < b − c тогда и только тогда, когда a < b.

LaTeX

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

Lean4

protected theorem tsub_lt_tsub_iff_right (hc : AddLECancellable c) (h : c ≤ a) : a - c < b - c ↔ a < b := by
  rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]

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