English
Let M be an additive monoid with a preorder and AddLeftStrictMono. Then the positive subset { x in M | 0 < x } inherits the property that left-translation reflects LT: if a < b with a,b > 0, then a + c < b + c for all c > 0.
Русский
Пусть M — аддитивный моноид с упорядочением и AddLeftStrictMono. Тогда множество положительных элементов наследует свойство отражения LT левым добавлением: если a < b и a,b > 0, то a + c < b + c для всех c > 0.
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\{ x \\\\in M \\\\mid 0 < x \\\\}, a < b \\\\Rightarrow a + c < b + c.$$$
Lean4
instance addLeftReflectLT [AddLeftReflectLT M] : AddLeftReflectLT { x : M // 0 < x } :=
⟨fun _ _ _ h => Subtype.coe_lt_coe.1 <| lt_of_add_lt_add_left h⟩
