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)

theorem le_pow_smul {G : Type u_4} [Monoid G] {α : Type u_5} [Preorder α] {g : G} {a : α} [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : a ≤ g • a) (n : ℕ) : a ≤ g ^ n • a

theorem pow_smul_le {G : Type u_4} [Monoid G] {α : Type u_5} [Preorder α] {g : G} {a : α} [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : g • a ≤ a) (n : ℕ) : g ^ n • a ≤ a