support_pow_le — Mathlib

English

For any permutation σ and natural number n, the support of σ^n is contained in the support of σ.

Русский

Для любой перестановки σ и натурального числа n опора σ^n содержится в опоре σ.

LaTeX

$$$\operatorname{supp}(\sigma^{n}) \subseteq \operatorname{supp}(\sigma).$$$

Lean4

theorem support_pow_le (σ : Perm α) (n : ℕ) : (σ ^ n).support ≤ σ.support := fun _ h1 =>
  mem_support.mpr fun h2 => mem_support.mp h1 (pow_apply_eq_self_of_apply_eq_self h2 n)

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