English
The derangements on Option α are equivalent to a sum over a of derangements on the complement of a and on α itself.
Русский
Деранджменты на Option α эквивалентны сумме по a из α derangements на комплемент a и на α.
LaTeX
$$$\operatorname{derangements}(\mathrm{Option}\, \alpha) \simeq \sum_{a:\alpha} (\operatorname{derangements}(({a}^{c} : \text{Set }\alpha)) \oplus \operatorname{derangements}(\alpha))$$$
Lean4
/-- The set of derangements on `Option α` is equivalent to the union over `a : α`
of "permutations with `a` the only possible fixed point". -/
def derangementsOptionEquivSigmaAtMostOneFixedPoint :
derangements (Option α) ≃ Σ a : α, {f : Perm α | fixedPoints f ⊆ { a }} :=
by
have fiber_none_is_false : Equiv.RemoveNone.fiber (@none α) → False :=
by
rw [Equiv.RemoveNone.fiber_none]
exact IsEmpty.false
calc
derangements (Option α) ≃ Equiv.Perm.decomposeOption '' derangements (Option α) := Equiv.image _ _
_ ≃ Σ a : Option α, ↥(Equiv.RemoveNone.fiber a) := (setProdEquivSigma _)
_ ≃ Σ a : α, ↥(Equiv.RemoveNone.fiber (some a)) := (sigmaOptionEquivOfSome _ fiber_none_is_false)
_ ≃ Σ a : α, {f : Perm α | fixedPoints f ⊆ { a }} :=
by
simp_rw [Equiv.RemoveNone.fiber_some]
rfl
