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 {M : Type u_2} {α : Type u_3} [Monoid M] [Preorder α] [MulAction M α] [CovariantClass M α HSMul.hSMul LE.le] {m : M} {a : α} (h : a ≤ m • a) (n : ℕ) : a ≤ m ^ n • a

theorem pow_smul_le {M : Type u_2} {α : Type u_3} [Monoid M] [Preorder α] [MulAction M α] [CovariantClass M α HSMul.hSMul LE.le] {m : M} {a : α} (h : m • a ≤ a) (n : ℕ) : m ^ n • a ≤ a

@[simp]

theorem smul_bot {α : Type u_3} {G : Type u_4} [Group G] [PartialOrder α] [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] [OrderBot α] (g : G) : g • ⊥ = ⊥

A group acting monotonically fixes ⊥.

@[simp]

theorem smul_top {α : Type u_3} {G : Type u_4} [Group G] [PartialOrder α] [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] [OrderTop α] (g : G) : g • ⊤ = ⊤

A group acting monotonically fixes ⊤.