lt_tsub_of_add_lt_left — Mathlib

English

Let α be a partially ordered additive cancellative semigroup with subtraction. If a is left-cancellable with respect to addition and a + c < b, then c < b − a.

Русский

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

LaTeX

$$$\text{LeftCancel}(a) \land a + c < b \Rightarrow c < b - a$$$

Lean4

protected theorem lt_tsub_of_add_lt_left (ha : AddLECancellable a) (h : a + c < b) : c < b - a :=
  ha.lt_tsub_of_add_lt_right <| by rwa [add_comm]

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