English
Let M be an additive monoid with a preorder and AddLeftStrictMono. Then the positive subset { x in M | 0 < x } has right translations that are strictly monotone: for any a>0 and b<c with b,c>0, b + a < c + a.
Русский
Пусть M — аддитивный моноид с упорядочением и AddLeftStrictMono. Тогда множество положительных элементов { x ∈ M | 0 < x } обладает правыми преобразованиями, которые строго монотонны: для любых a>0 и b<c выполняется b + a < c + a.
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\{ x \\\\in M \\\\mid 0 < x \\\\}, b < c \\\\Rightarrow b + a < c + a.$$$
Lean4
instance addRightStrictMono [AddRightStrictMono M] : AddRightStrictMono { x : M // 0 < x } :=
⟨fun _ y z hyz => Subtype.coe_lt_coe.1 <| add_lt_add_right (show (y : M) < z from hyz) _⟩
