English
Every permutation of Fin(n+1) can be obtained by taking a pair (p,e) with p ∈ Fin(n+1) and e ∈ Perm(Fin n) and applying decomposeFin.symm.
Русский
Каждая перестановка Fin(n+1) получается как (p,e) с p ∈ Fin(n+1) и e ∈ Perm(Fin n) через decomposeFin.symm.
LaTeX
$$$ \\mathrm{Perm}(\\mathrm{Fin}(n+1)) \\cong \\mathrm{Fin}(n+1) \\times \\mathrm{Perm}(\\mathrm{Fin}\\,n) \\quad (p,e) \\mapsto \\mathrm{decomposeFin.symm}(p,e)$$$
Lean4
/-- The set of all permutations of `Fin (n + 1)` can be constructed by augmenting the set of
permutations of `Fin n` by each element of `Fin (n + 1)` in turn. -/
theorem univ_perm_fin_succ {n : ℕ} :
@Finset.univ (Perm <| Fin n.succ) _ =
(Finset.univ : Finset <| Fin n.succ × Perm (Fin n)).map Equiv.Perm.decomposeFin.symm.toEmbedding :=
(Finset.univ_map_equiv_to_embedding _).symm
