English
Permutations of Option α are in bijection with pairs consisting of an element of Option α and a permutation of α; this is given by σ ↦ (σ none, removing the None-structure).
Русский
Перестановки над Option α эквивалентны парам вида (элемент в Option α, перестановка α); задаётся отображением σ ↦ (σ none, removeNone σ).
LaTeX
$$$ \\mathrm{Perm}(\\mathrm{Option}(\\alpha)) \\simeq \\mathrm{Option}(\\alpha) \\times \\mathrm{Perm}(\\alpha) $$$
Lean4
/-- Permutations of `Option α` are equivalent to fixing an
`Option α` and permuting the remaining with a `Perm α`.
The fixed `Option α` is swapped with `none`. -/
@[simps]
def decomposeOption {α : Type*} [DecidableEq α] : Perm (Option α) ≃ Option α × Perm α
where
toFun σ := (σ none, removeNone σ)
invFun i := swap none i.1 * i.2.optionCongr
left_inv σ := by simp
right_inv := fun ⟨x, σ⟩ =>
by
have : removeNone (swap none x * σ.optionCongr) = σ := Equiv.optionCongr_injective (by simp [← mul_assoc])
simp [this]
