English
If c ∈ g.cycleFactorsFinset, then applying g does not change the membership of elements in c.support: g a ∈ c.support iff a ∈ c.support.
Русский
Если c ∈ cycleFactorsFinset g, то применение g не меняет принадлежность элемента к опоре c: g a ∈ c.support ↔ a ∈ c.support.
LaTeX
$$$\forall g,c : \mathrm{Perm}(\alpha),\; (hc : c \in g.\mathrm{cycleFactorsFinset})\;\forall a:\alpha,\; g a \in c.\mathrm{support} \iff a \in c.\mathrm{support}$$$
Lean4
/-- If a permutation is a cycle of `g`, then its support is invariant under `g`. -/
theorem mem_cycleFactorsFinset_support {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (a : α) :
g a ∈ c.support ↔ a ∈ c.support :=
mem_support_iff_of_commute (self_mem_cycle_factors_commute hc).symm a