Module docstring
{"# 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. "}
smul_mono_right
theorem
[SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) : Monotone (HSMul.hSMul m : α → α)
Full source
theorem smul_mono_right [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le]
(m : M) : Monotone (HSMul.hSMul m : α → α) :=
fun _ _ => CovariantClass.elim _Informal description
Let $M$ be a type equipped with a scalar multiplication action on a type $\alpha$, where $\alpha$ is equipped with a preorder. If the action is covariant with respect to the less-than-or-equal relation (i.e., for any $m \in M$, the function $x \mapsto m \cdot x$ preserves the order), then for any $m \in M$, the function $x \mapsto m \cdot x$ is monotone.
smul_le_smul_left
theorem
[SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) {a b : α} (h : a ≤ b) : m • a ≤ m • b
Full source
/-- 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 _ hInformal description
Let $M$ be a type with a scalar multiplication action on a preordered type $\alpha$, where the action is covariant with respect to the order (i.e., for any $m \in M$, the function $x \mapsto m \cdot x$ is order-preserving). Then for any $m \in M$ and any $a, b \in \alpha$ with $a \leq b$, we have $m \cdot a \leq m \cdot b$.
smul_inf_le
theorem
[SMul M α] [SemilatticeInf α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) (a₁ a₂ : α) :
m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂
Full source
theorem smul_inf_le [SMul M α] [SemilatticeInf α] [CovariantClass M α HSMul.hSMul LE.le]
(m : M) (a₁ a₂ : α) : m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂ :=
(smul_mono_right _).map_inf_le _ _Informal description
Let $M$ be a type with a scalar multiplication action on a meet-semilattice $\alpha$, where the action is covariant with respect to the order (i.e., for any $m \in M$, the function $x \mapsto m \cdot x$ is order-preserving). Then for any $m \in M$ and any $a_1, a_2 \in \alpha$, we have the inequality:
\[ m \cdot (a_1 \sqcap a_2) \leq (m \cdot a_1) \sqcap (m \cdot a_2). \]
smul_iInf_le
theorem
[SMul M α] [CompleteLattice α] [CovariantClass M α HSMul.hSMul LE.le] {m : M} {t : ι → α} : m • iInf t ≤ ⨅ i, m • t i
Full source
theorem smul_iInf_le [SMul M α] [CompleteLattice α] [CovariantClass M α HSMul.hSMul LE.le]
{m : M} {t : ι → α} :
m • iInf t ≤ ⨅ i, m • t i :=
le_iInf fun _ => smul_mono_right _ (iInf_le _ _)Informal description
Let $M$ be a type with a scalar multiplication action on a complete lattice $\alpha$, where the action is covariant with respect to the less-than-or-equal relation (i.e., for any $m \in M$, the function $x \mapsto m \cdot x$ is order-preserving). Then for any $m \in M$ and any indexed family $t : \iota \to \alpha$, we have the inequality:
\[ m \cdot \left(\bigsqcap_i t_i\right) \leq \bigsqcap_i (m \cdot t_i). \]
smul_strictMono_right
theorem
[SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LT.lt] (m : M) : StrictMono (HSMul.hSMul m : α → α)
Full source
theorem smul_strictMono_right [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LT.lt]
(m : M) : StrictMono (HSMul.hSMul m : α → α) :=
fun _ _ => CovariantClass.elim _Informal description
Let $M$ be a type with a scalar multiplication operation on a type $\alpha$, where $\alpha$ is equipped with a preorder. If the scalar multiplication is covariant with respect to the strict less-than relation $<$ (i.e., for any $m \in M$, the function $x \mapsto m \cdot x$ preserves strict inequalities), then for any $m \in M$, the function $x \mapsto m \cdot x$ is strictly monotone.
le_pow_smul
theorem
{G : Type*} [Monoid G] {α : Type*} [Preorder α] {g : G} {a : α} [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le]
(h : a ≤ g • a) (n : ℕ) : a ≤ g ^ n • a
Full source
lemma le_pow_smul {G : Type*} [Monoid G] {α : Type*} [Preorder α] {g : G} {a : α}
[MulAction G α] [CovariantClass G α HSMul.hSMul LE.le]
(h : a ≤ g • a) (n : ℕ) : a ≤ g ^ n • a := by
induction n with
| zero => rw [pow_zero, one_smul]
| succ n hn =>
rw [pow_succ', mul_smul]
exact h.trans (smul_mono_right g hn)Informal description
Let $G$ be a monoid acting on a preordered set $\alpha$ via scalar multiplication, and suppose this action is covariant with respect to the less-than-or-equal relation (i.e., for any $g \in G$, the function $x \mapsto g \cdot x$ is monotone). If $a \leq g \cdot a$ for some $g \in G$ and $a \in \alpha$, then for any natural number $n$, it holds that $a \leq g^n \cdot a$.
pow_smul_le
theorem
{G : Type*} [Monoid G] {α : Type*} [Preorder α] {g : G} {a : α} [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le]
(h : g • a ≤ a) (n : ℕ) : g ^ n • a ≤ a
Full source
lemma pow_smul_le {G : Type*} [Monoid G] {α : Type*} [Preorder α] {g : G} {a : α}
[MulAction G α] [CovariantClass G α HSMul.hSMul LE.le]
(h : g • a ≤ a) (n : ℕ) : g ^ n • a ≤ a := by
induction n with
| zero => rw [pow_zero, one_smul]
| succ n hn =>
rw [pow_succ', mul_smul]
exact (smul_mono_right g hn).trans hInformal description
Let $G$ be a monoid acting on a preordered set $\alpha$ such that the action is covariant with respect to the less-than-or-equal relation (i.e., for any $g \in G$, the function $x \mapsto g \cdot x$ is monotone). If $g \cdot a \leq a$ for some $g \in G$ and $a \in \alpha$, then for any natural number $n$, we have $g^n \cdot a \leq a$.