Finset.univ_perm_option

theorem Finset.univ_perm_option : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Finset.univ = Finset.map Equiv.Perm.decomposeOption.symm.toEmbedding Finset.univ

This theorem states that the set of all permutations of `Option α` can be constructed by extending the set of permutations of `α` with each element of `Option α` sequentially. In other words, for any type `α` that has decidable equality and is a finite type, the universal finset of permutations of `Option α` is equivalent to the image of the universal finset of `α` under the embedding induced by the inverse of the function `Equiv.Perm.decomposeOption`. This demonstrates a relationship between the permutations of a type `α` and the permutations of the type `Option α`, which includes the elements of `α` and an additional `None` option.

More concisely: The set of permutations of `Option α` is equivalent to the image of the universal set of permutations of `α` under the embedding induced by the inverse of `Equiv.Perm.decomposeOption`, for finite types `α` with decidable equality.