instDecidablePredPermDerangements

English

Let α be a finite set endowed with a decidable equality. Then the collection of derangements on α is a decidable predicate, i.e. there exists a computable test that decides whether a given permutation of α has no fixed points.

Русский

Пусть α — конечное множество с обусловленным равенством. Тогда множество перестановок без фиксации точек на α образует разрешимый предикат, то есть существует вычислимая проверка принадлежности перестановки к этому множеству.

LaTeX

$$$\\exists D:\\mathrm{Perm}(\\alpha) \\to \\{0,1\\},\\ D(\\sigma)=1 \\iff \\forall x\\in\\alpha,\\ \\sigma(x)\\neq x.$$$

Lean4

instance : DecidablePred (derangements α) := fun _ => Fintype.decidableForallFintype

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