sort — Mathlib

English

Sort f is the permutation that orders Fin n according to the order of the outputs of f.

Русский

Sort f — перестановка, упорядочивающая Fin n по возрастанию значений f(i).

LaTeX

$$$\\mathrm{sort}(f) \\in \\mathrm{Equiv}(\\mathrm{Fin}\\,n,\\mathrm{Fin}\\,n)$ and $f \\circ \\mathrm{sort}(f)$ is monotone.$$

Lean4

/-- `sort f` is the permutation that orders `Fin n` according to the order of the outputs of `f`. -/
def sort (f : Fin n → α) : Equiv.Perm (Fin n) :=
  (graphEquiv₂ f).toEquiv.trans (graphEquiv₁ f).symm

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