@[simp]
theorem
equiv.option_congr_swap
{α : Type u_1}
[decidable_eq α]
(x y : α) :
equiv.option_congr (equiv.swap x y) = equiv.swap (some x) (some y)
@[simp]
@[simp]
theorem
map_equiv_remove_none
{α : Type u_1}
[decidable_eq α]
(σ : equiv.perm (option α)) :
(equiv.remove_none σ).option_congr = (equiv.swap none (⇑σ 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 α)), (⇑σ none, equiv.remove_none σ), inv_fun := λ (i : option α × equiv.perm α), (equiv.swap 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 α) :
⇑(equiv.perm.decompose_option.symm) i = (equiv.swap none i.fst) * equiv.option_congr i.snd
theorem
equiv.perm.decompose_option_symm_of_none_apply
{α : Type u_1}
[decidable_eq α]
(e : equiv.perm α)
(i : option α) :
⇑(⇑(equiv.perm.decompose_option.symm) (none α, e)) i = option.map ⇑e i
theorem
equiv.perm.decompose_option_symm_sign
{α : Type u_1}
[decidable_eq α]
[fintype α]
(e : equiv.perm α) :
⇑equiv.perm.sign (⇑(equiv.perm.decompose_option.symm) (none α, e)) = ⇑equiv.perm.sign e
The set of all permutations of option α can be constructed by augmenting the set of
permutations of α by each element of option α in turn.