English
Let g be a permutation of a finite type α and c be a cycle factor of g. For any integer m, the support of c is invariant under the m-th power of g; equivalently, for every x, (g^m)(x) lies in the support of c if and only if x lies in the support of c.
Русский
Пусть g — перестановка над конечным множеством α, и c — цикл-фактор g. Для любого целого m опора c сохраняется под возведением g в степень m; то есть для каждого x выполняется: (g^m)(x) принадлежит опоре c тогда и только если x принадлежит опоре c.
LaTeX
$$$\forall g : \mathrm{Perm}(\alpha)\,\forall x: \alpha\,\forall m : \mathbb{Z}\,\forall c \in g.cycleFactorsFinset, (g^m)\,x \in (c : \mathrm{Perm}(\alpha)).\mathrm{support} \iff x \in (c : \mathrm{Perm}(\alpha)).\mathrm{support}$$$
Lean4
theorem zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff {g : Perm α} {x : α} {m : ℤ} {c : g.cycleFactorsFinset} :
(g ^ m) x ∈ (c : Perm α).support ↔ x ∈ (c : Perm α).support := by
rw [← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop, cycleOf_self_apply_zpow,
eq_cycleOf_of_mem_cycleFactorsFinset_iff _ _ c.prop]
