fiber — Mathlib

English

Derangements on the option type decompose as a sigma-type over α: for each a in α, derangements with fixedPoints ⊆ {a}.

Русский

Деранджменты на Option α разлагаются по α: для каждого a в α существуют дерangements с fixedPoints ⊆ {a}.

LaTeX

$$$\operatorname{derangements}(\mathrm{Option}\, \alpha) \simeq \sum_{a:\alpha} \{ f: \mathrm{Perm}\, \alpha \mid \operatorname{fixedPoints}(f) \subseteq \{a\} \}$$$

Lean4

/-- The set of permutations `f` such that the preimage of `(a, f)` under
`Equiv.Perm.decomposeOption` is a derangement. -/
def fiber (a : Option α) : Set (Perm α) :=
  {f : Perm α | (a, f) ∈ Equiv.Perm.decomposeOption '' derangements (Option α)}

Похожие утверждения