English
Let M be an additive monoid with a partial order and AddLeftStrictMono. Then the positive subset { x in M | 0 < x } is AddLeftMono, i.e., for any a>0 and b ≤ c, a + b ≤ a + c.
Русский
Пусть M — аддитивный моноид с частичным порядком и AddLeftStrictMono. Тогда множество положительных элементов { x ∈ M | 0 < x } образует AddLeftMono: для любого a>0 и b ≤ c выполняется a + b ≤ a + c.
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\{ x \\\\in M \\\\mid 0 < x \\\\}, b \\\\le c \\\\Rightarrow a + b \\\\le a + c.$$$
Lean4
instance addLeftMono [AddMonoid M] [PartialOrder M] [AddLeftStrictMono M] : AddLeftMono { x : M // 0 < x } :=
⟨@fun _ _ _ h₁ => StrictMono.monotone (fun _ _ h => add_lt_add_left h _) h₁⟩
