smul_mono_right — Mathlib

English

For any M acting on α with a CovariantClass in the right, the map x ↦ m • x is monotone in x.

Русский

При наличии соответствующего ковариантного класса отображение x ↦ m • x монотонно по x.

LaTeX

$$$ \\forall a,b\\in α, \\, a \\le b \\Rightarrow m \\cdot a \\le m \\cdot b. $$$

Lean4

theorem smul_mono_right [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) :
    Monotone (HSMul.hSMul m : α → α) := fun _ _ => CovariantClass.elim _

Похожие утверждения