derangements — Mathlib

English

The derangements on a subtype are equivalent to a permutation data on the ambient set with a fixed points condition.

Русский

Деранджменты на подмножествах эквивалентны перестановкам на всей области с учётом фиксированных точек.

LaTeX

$$$\text{derangements}(\text{Subtype } p) \simeq { f: \text{Perm } \alpha \mid \forall a, \lnot p(a) \Rightarrow a \in \text{fixedPoints}(f) }$$$

Lean4

/-- A permutation is a derangement if it has no fixed points. -/
def derangements (α : Type*) : Set (Perm α) :=
  {f : Perm α | ∀ x : α, f x ≠ x}

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