mem_derangements_iff_fixedPoints_eq_empty

English

A permutation lies in the derangements on α exactly when it has no fixed points, i.e., fixedPoints is empty.

Русский

Перестановка входит в множество дерangements α тогда и только тогда, когда у неё нет зафиксированных точек.

LaTeX

$$$ f \in \text{derangements}(\alpha) \iff \text{fixedPoints}(f) = \emptyset $$$

Lean4

theorem mem_derangements_iff_fixedPoints_eq_empty {f : Perm α} : f ∈ derangements α ↔ fixedPoints f = ∅ :=
  Set.eq_empty_iff_forall_notMem.symm

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