tsub_lt_tsub_iff_left_of_le — Mathlib

English

If a and b are cancellable and h : b ≤ a, then a − b < a − c ↔ c < b.

Русский

Если a и b удовлетворяют условию отменяемости и h: b ≤ a, то a − b < a − c ↔ c < b.

LaTeX

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

Lean4

/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
theorem tsub_lt_tsub_iff_left_of_le (h : b ≤ a) : a - b < a - c ↔ c < b :=
  Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le Contravariant.AddLECancellable h

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