English
If a ≤ g • a for a Monoid G acting on α with CovariantClass, then a ≤ g^n • a for all n ∈ ℕ.
Русский
Если a ≤ g • a и действует на α группа G (моноид), то для всех n ∈ ℕ выполняется a ≤ g^n • a.
LaTeX
$$$ {G : Type*} [Monoid G] {\\alpha : Type*} [Preorder \\alpha] {g : G} {a : \\alpha} [MulAction G \\alpha] [CovariantClass G α HSMul.hSMul LE.le] (h : a \\le g \\cdot a) (n : \\mathbb{N}) : a \\le g^n \\cdot a. $$$
Lean4
theorem 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)
