lt_tsub_iff_left — Mathlib

English

Let α be a linearly ordered canonically ordered additive monoid with a subtraction operation. If c is cancellable from the left (with respect to addition), then for all a,b we have a < b − c if and only if c + a < b.

Русский

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

LaTeX

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

Lean4

protected theorem lt_tsub_iff_left (hc : AddLECancellable c) : a < b - c ↔ c + a < b :=
  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_left.mpr, hc.lt_tsub_of_add_lt_left⟩

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