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 right-translation reflects LT: if a < b with a,b > 0, then c + a < c + b for all c > 0.
Русский
Пусть M — аддитивный моноид с упорядочением и AddLeftStrictMono. Тогда множество положительных элементов наследует свойство отражения LT правым добавлением: если a < b и a,b > 0, то c + a < c + b для всех c > 0.
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\{ x \\\\in M \\\\mid 0 < x \\\\}, a < b \\\\Rightarrow c + a < c + b.$$$
Lean4
instance addRightReflectLT [AddRightReflectLT M] : AddRightReflectLT { x : M // 0 < x } :=
⟨fun _ _ _ h => Subtype.coe_lt_coe.1 <| lt_of_add_lt_add_right h⟩
