English
The universal set of permutations on Option α is obtained by mapping the universal set of pairs (Option α, Perm α) through the decomposeOption symmetry.
Русский
Единственный множества перестановок над Option α получается как отображение единичного множества пар (Option α, Perm α) через тождество-изоморфизм decomposeOption.
LaTeX
$$$ \\mathrm{Finset.univ}(\\mathrm{Perm}(\\mathrm{Option}(\\alpha))) = (\\mathrm{Finset.univ} : \\mathrm{Finset}(\\mathrm{Option}(\\alpha) \\times \\mathrm{Perm}(\\alpha))).map(\\mathrm{Equiv.Perm.decomposeOption.symm.toEmbedding) $$$
Lean4
/-- The set of all permutations of `Option α` can be constructed by augmenting the set of
permutations of `α` by each element of `Option α` in turn. -/
theorem univ_perm_option {α : Type*} [DecidableEq α] [Fintype α] :
@Finset.univ (Perm <| Option α) _ =
(Finset.univ : Finset <| Option α × Perm α).map Equiv.Perm.decomposeOption.symm.toEmbedding :=
(Finset.univ_map_equiv_to_embedding _).symm
