Results about CovariantClass G α HSMul.hSMul LE.le

When working with group actions rather than modules, we drop the 0 < c condition.

Notably these are relevant for pointwise actions on set-like objects.

theorem smul_mono_right {M : Type u_2} {α : Type u_3} [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) : Monotone (HSMul.hSMul m)

theorem smul_le_smul_left {M : Type u_2} {α : Type u_3} [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) {a : α} {b : α} (h : a ≤ b) : m • a ≤ m • b

A copy of smul_mono_right that is understood by gcongr.

theorem smul_inf_le {M : Type u_2} {α : Type u_3} [SMul M α] [SemilatticeInf α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) (a₁ : α) (a₂ : α) : m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂

theorem smul_iInf_le {ι : Sort u_1} {M : Type u_2} {α : Type u_3} [SMul M α] [CompleteLattice α] [CovariantClass M α HSMul.hSMul LE.le] {m : M} {t : ι → α} : m • iInf t ≤ ⨅ (i : ι), m • t i

theorem smul_strictMono_right {M : Type u_2} {α : Type u_3} [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LT.lt] (m : M) : StrictMono (HSMul.hSMul m)