English
The action of NNReal on a preorder α with a strictly monotone real action is itself strictly monotone from the left: a ≤ b implies r • a ≤ r • b for r ≥ 0, and strict if a < b.
Русский
Действие NNReal на частично упорядоченном множестве α с строго монотонным действием на ℝ сохраняет строгую монотонность слева: если a < b, то r • a < r • b при r ≥ 0.
LaTeX
$$$ \\text{If } α \\text{ has a Preorder and a left action by } \\mathbb{R}, \\; \\text{and } \\text{PosSMulStrictMono } \\mathbb{R} \\; α, \\text{ then } NNReal \\text{ acts with } \\text{PosSMulStrictMono } α. $$$
Lean4
instance instPosSMulStrictMono {α} [Preorder α] [MulAction ℝ α] [PosSMulStrictMono ℝ α] : PosSMulStrictMono ℝ≥0 α where
smul_lt_smul_of_pos_left _r hr _a₁ _a₂ ha := (smul_lt_smul_of_pos_left ha (coe_pos.2 hr) :)
