smul_strictMono_right — Mathlib

English

For any M α with a CovariantClass on LT.lt, the map x ↦ m • x is StrictMono.

Русский

Для любого M α с ковариантным классом относительно LT.lt отображение x ↦ m • x является StrictMono.

LaTeX

$$$ [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LT.lt] (m : M) :\\n StrictMono (HSMul.hSMul m : α \\to α). $$$

Lean4

theorem smul_strictMono_right [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LT.lt] (m : M) :
    StrictMono (HSMul.hSMul m : α → α) := fun _ _ => CovariantClass.elim _

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