English
Given a finset s, the finset permsOfFinset(s) lists all permutations of its elements.
Русский
Для данного конечного множества s формируется множество permsOfFinset(s), содержащее все перестановки его элементов.
LaTeX
$$$\\mathrm{permsOfFinset}(s) \\subseteq \\mathrm{Perm}(\\alpha) \\text{ enumerates all permutations of } s.$$$
Lean4
/-- Given a finset, produce the finset of all permutations of its elements. -/
def permsOfFinset (s : Finset α) : Finset (Perm α) :=
Quotient.hrecOn s.1 (fun l hl => ⟨permsOfList l, nodup_permsOfList hl⟩)
(fun a b hab =>
hfunext (congr_arg _ (Quotient.sound hab)) fun ha hb _ =>
heq_of_eq <| Finset.ext <| by simp [mem_permsOfList_iff, hab.mem_iff])
s.2
