rev — Mathlib

English

rev i flips Fin2 n by mapping 0 → last and (fs k) → (rev k).castSucc.

Русский

rev разворотит Fin2 n: 0 → last, fs k → (rev k).castSucc.

LaTeX

$$$\text{rev} : \forall n,\mathrm{Fin2} n \to \mathrm{Fin2} n,\; \mathrm{rev}(\mathrm{fz}) = \text{last},\; \mathrm{rev}(\mathrm{fs}\ i) = \mathrm{fs}(\mathrm{rev}\ i).castSucc$$$

Lean4

/-- Maps `0` to `n-1`, `1` to `n-2`, ..., `n-1` to `0`. -/
def rev {n : Nat} : Fin2 n → Fin2 n
  | .fz => last
  | .fs i => i.rev.castSucc

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