revPerm — Mathlib

English

There is a reversal permutation of Fin(n); the map rev defines a permutation of Fin(n).

Русский

Существует перестановка разворота Fin(n); отображение rev задаёт перестановку Fin(n).

LaTeX

$$$\mathrm{revPerm} : \mathrm{Equiv.Perm}(\mathrm{Fin}(n)).$$$

Lean4

/-- `Fin.rev` as an `Equiv.Perm`, the antitone involution `Fin n → Fin n` given by
`i ↦ n-(i+1)`. -/
@[simps! apply symm_apply]
def revPerm : Equiv.Perm (Fin n) :=
  Involutive.toPerm rev rev_involutive

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