English
A permutation p belongs to the cycle factors of f iff p is a cycle and p coincides with f on its support.
Русский
Перестановка p принадлежит факторным циклам f тогда и только тогда, когда p — цикл и p совпадает с f на опорном множестве.
LaTeX
$$$p \in cycleFactorsFinset(f) \\iff p.IsCycle \land \forall a \in p.support, p(a)=f(a)$$$
Lean4
theorem mem_cycleFactorsFinset_iff {f p : Perm α} : p ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a :=
by
obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
rw [← hl']
rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
simpa [List.mem_toFinset, Ne, ← hl'.right.right] using mem_list_cycles_iff hl'.left hl'.right.left