support_zpow_le — Mathlib

English

For a permutation σ and integer 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_zpow_le (σ : Perm α) (n : ℤ) : (σ ^ n).support ≤ σ.support := fun _ h1 =>
  mem_support.mpr fun h2 => mem_support.mp h1 (zpow_apply_eq_self_of_apply_eq_self h2 n)

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