Permutations of Option α

@[simp]

theorem Equiv.optionCongr_one {α : Type u_1} : Equiv.optionCongr 1 = 1

@[simp]

theorem Equiv.optionCongr_swap {α : Type u_1} [DecidableEq α] (x : α) (y : α) : Equiv.optionCongr (Equiv.swap x y) = Equiv.swap (some x) (some y)

@[simp]

theorem Equiv.optionCongr_sign {α : Type u_1} [DecidableEq α] [Fintype α] (e : Equiv.Perm α) : ↑Equiv.Perm.sign (Equiv.optionCongr e) = ↑Equiv.Perm.sign e

@[simp]

theorem map_equiv_removeNone {α : Type u_1} [DecidableEq α] (σ : Equiv.Perm (Option α)) : Equiv.optionCongr (Equiv.removeNone σ) = Equiv.swap none (↑σ none) * σ

@[simp]

theorem Equiv.Perm.decomposeOption_apply {α : Type u_1} [DecidableEq α] (σ : Equiv.Perm (Option α)) : ↑Equiv.Perm.decomposeOption σ = (↑σ none, Equiv.removeNone σ)

@[simp]

theorem Equiv.Perm.decomposeOption_symm_apply {α : Type u_1} [DecidableEq α] (i : Option α × Equiv.Perm α) : ↑Equiv.Perm.decomposeOption.symm i = Equiv.swap none i.fst * Equiv.optionCongr i.snd

def Equiv.Perm.decomposeOption {α : Type u_1} [DecidableEq α] : Equiv.Perm (Option α) ≃ Option α × Equiv.Perm α

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

Equations

• One or more equations did not get rendered due to their size.

theorem Equiv.Perm.decomposeOption_symm_of_none_apply {α : Type u_1} [DecidableEq α] (e : Equiv.Perm α) (i : Option α) : ↑(↑Equiv.Perm.decomposeOption.symm (none, e)) i = Option.map (↑e) i

theorem Equiv.Perm.decomposeOption_symm_sign {α : Type u_1} [DecidableEq α] [Fintype α] (e : Equiv.Perm α) : ↑Equiv.Perm.sign (↑Equiv.Perm.decomposeOption.symm (none, e)) = ↑Equiv.Perm.sign e

theorem Finset.univ_perm_option {α : Type u_1} [DecidableEq α] [Fintype α] : Finset.univ = Finset.map (Equiv.toEmbedding Equiv.Perm.decomposeOption.symm) Finset.univ

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