English
For a finite set s, there exists a cycle f with IsCycleOn s and support contained in s.
Русский
Для конечного множества s существует цикл f, удовлетворяющий IsCycleOn s и опоре в s.
LaTeX
$$$\text{Finite}(s) \Rightarrow \exists f:\mathrm{Perm}(\alpha), f.IsCycleOn(s) \land \mathrm{supp}(f) \subseteq s$$$
Lean4
theorem product_self_eq_disjiUnion_perm_aux (hf : f.IsCycleOn s) :
(range #s : Set ℕ).PairwiseDisjoint fun k => s.map ⟨fun i => (i, (f ^ k) i), fun _ _ => congr_arg Prod.fst⟩ :=
by
obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
· refine Set.Subsingleton.pairwise ?_ _
simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢
rwa [card_range]
classical
rintro m hm n hn hmn
simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk, not_exists, not_and,
forall_exists_index, and_imp, Prod.forall, Prod.mk_inj]
rintro _ _ _ - rfl rfl a ha rfl h
rw [hf.pow_apply_eq_pow_apply ha] at h
rw [mem_coe, mem_range] at hm hn
exact hmn.symm (h.eq_of_lt_of_lt hn hm)
