mathlib3 documentation


Permutations of option α #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem equiv.option_congr_one {α : Type u_1} :

Permutations of option α are equivalent to fixing an option α and permuting the remaining with a perm α. The fixed option α is swapped with none.


The set of all permutations of option α can be constructed by augmenting the set of permutations of α by each element of option α in turn.