pow_smul_le — Mathlib

English

If g · a ≤ a, then g^n · a ≤ a for all n ∈ ℕ.

Русский

Если g · a ≤ a, то g^n · a ≤ a для всех n ∈ ℕ.

LaTeX

$$$ {G : Type*} [Monoid G] {\\alpha : Type*} [Preorder \\alpha] {g : G} {a : \\alpha} [MulAction G α] [CovariantClass G α HSMul LE.le] (h : g \\cdot a \\le a) (n : \\mathbb{N}) : g^n \\cdot a \\le a. $$$

Lean4

theorem 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 h

Похожие утверждения