Permutations of option α #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
theorem
equiv.option_congr_swap
{α : Type u_1}
[decidable_eq α]
(x y : α) :
equiv.option_congr (equiv.swap x y) = equiv.swap (option.some x) (option.some y)
@[simp]
@[simp]
theorem
map_equiv_remove_none
{α : Type u_1}
[decidable_eq α]
(σ : equiv.perm (option α)) :
(equiv.remove_none σ).option_congr = equiv.swap option.none (⇑σ option.none) * σ
def
equiv.perm.decompose_option
{α : Type u_1}
[decidable_eq α] :
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
- equiv.perm.decompose_option = {to_fun := λ (σ : equiv.perm (option α)), (⇑σ option.none, equiv.remove_none σ), inv_fun := λ (i : option α × equiv.perm α), equiv.swap option.none i.fst * equiv.option_congr i.snd, left_inv := _, right_inv := _}
@[simp]
theorem
equiv.perm.decompose_option_apply
{α : Type u_1}
[decidable_eq α]
(σ : equiv.perm (option α)) :
@[simp]
theorem
equiv.perm.decompose_option_symm_apply
{α : Type u_1}
[decidable_eq α]
(i : option α × equiv.perm α) :
theorem
equiv.perm.decompose_option_symm_of_none_apply
{α : Type u_1}
[decidable_eq α]
(e : equiv.perm α)
(i : option α) :
⇑(⇑(equiv.perm.decompose_option.symm) (option.none α, e)) i = option.map ⇑e i
theorem
equiv.perm.decompose_option_symm_sign
{α : Type u_1}
[decidable_eq α]
[fintype α]
(e : equiv.perm α) :
The set of all permutations of option α can be constructed by augmenting the set of
permutations of α by each element of option α in turn.