perm_pow — Mathlib

English

If f is a permutation of α acting on a set s and maps s into s, then all powers f^n also map s into s for any natural n.

Русский

Если f — перестановка α, отображающая множество s в s, то и все степени f^n отображают s в s.

LaTeX

$$MapsTo f s s → ∀ n, MapsTo (f ^ n) s s$$

Lean4

theorem perm_pow : MapsTo f s s → ∀ n : ℕ, MapsTo (f ^ n) s s := by simp_rw [Equiv.Perm.coe_pow]; exact MapsTo.iterate

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