instPosSMulStrictMono — Mathlib

English

If α is ordered and β is a module, then scalar action on finsupp is strictly monotone with respect to the scalar.

Русский

Если α упорядочен и β модуль, то скалярное действие на finsupp строго монотонно по скаляру.

LaTeX

$$PosSMulStrictMono α (ι →₀ β)$$

Lean4

instance instPosSMulStrictMono [PosSMulStrictMono α β] : PosSMulStrictMono α (ι →₀ β) :=
  PosSMulStrictMono.lift _ coe_le_coe coe_smul

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