English
For any countable s, there exists f a permutation of α that is a cycle on s with support contained in s.
Русский
Для счётного s существует перестановка f на α, которая образует цикл на s и опора лежит в s.
LaTeX
$$$\mathrm{Set.Countable}(s) \Rightarrow \exists f:\mathrm{Perm}(\alpha), f.IsCycleOn(s) \land \mathrm{supp}(f) \subseteq s$$$
Lean4
theorem exists_cycleOn (hs : s.Countable) : ∃ f : Perm α, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s := by
classical
obtain hs' | hs' := s.finite_or_infinite
· refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by simpa using List.mem_of_formPerm_apply_ne hx⟩
convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
simp
· haveI := hs.to_subtype
haveI := hs'.to_subtype
obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
refine
⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
convert Int.addRight_one_isCycle.isCycleOn.extendDomain f
rw [Set.image_comp, Equiv.image_eq_preimage]
ext
simp
