English
Let α be a set and p a predicate on α. Suppose f is a permutation of α that preserves p, i.e. p(f(x)) holds iff p(x) holds for all x. Then restricting f to the subset {x ∈ α : p(x)} and taking integer powers commutes with restriction: for every integer n, the n-th power of the restricted permutation equals the restriction of the n-th power of f.
Русский
Пусть α множество, p – предикат на α, и f – перестановка α, сохраняющая p, то есть p(f(x)) эквивалентно p(x) для всех x. Тогда restricting на подмножество {x ∈ α : p(x)} и возведение в целочисленную степень коммутируют: для любого n ∈ ℤ верно, что n-я сила ограничения равна ограничению n-й силы f.
LaTeX
$$$ \\forall n \\in \\mathbb{Z},\\;(f|_p)^n = (f^n)|_p \\quad\\text{as permutations of }\\{x \\in \\alpha \\mid p(x)\\}. $$$
Lean4
@[simp]
theorem subtypePerm_zpow (f : Perm α) (n : ℤ) (hf) :
(f.subtypePerm hf ^ n : Perm { x // p x }) = (f ^ n).subtypePerm (zpow_aux hf) := by
cases n with
| ofNat n => exact subtypePerm_pow _ _ _
| negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]
