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