smul_le_smul_left — Mathlib

English

If a ≤ b, then m • a ≤ m • b for any m ∈ M under the appropriate CovariantClass.

Русский

Если a ≤ b, то m • a ≤ m • b при заданном ковариантном классе действия.

LaTeX

$$$ [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) {a \\ b : α} (h : a \\le b) : m \\cdot a \\le m \\cdot b. $$$

Lean4

/-- A copy of `smul_mono_right` that is understood by `gcongr`. -/
@[gcongr]
theorem smul_le_smul_left [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) {a b : α} (h : a ≤ b) :
    m • a ≤ m • b :=
  smul_mono_right _ h

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