rev_involutive — Mathlib

English

For every natural n, the reverse operation on Fin(n) is an involution; applying it twice yields the identity.

Русский

Для каждого натурального n операция разворота на Fin(n) является инволюцией; применение её дважды даёт тождественную отображение.

LaTeX

$$$\forall n,\; (\mathrm{rev}_n)^{2} = \mathrm{id}_{\mathrm{Fin}(n)}$$$

Lean4

theorem rev_involutive {n} : Function.Involutive (@rev n) :=
  rev_rev

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