English
There is a canonical embedding of the standard index type Fin n into the alternative Fin2 n, defined by sending 0 to the bottom element and associating successor indices with the successor element. Concretely, define ofFin: Fin n → Fin2 n by ofFin(0) = fz and ofFin(i.succ) = fs(ofFin(i)).
Русский
Существуют стандартное встраивание типа индексов Fin n в альтернативное Fin2 n, задаваемое так: 0 соответствует нижнему элементу, а переход черезsucc соответствует переходу к следующему элементу. Конкретно: ofFin: Fin n → Fin2 n удовлетворяет ofFin(0) = fz и ofFin(i.succ) = fs(ofFin(i)).
LaTeX
$$$\mathrm{Fin2\text{-}ofFin}(0) = \mathrm{fz}, \quad \mathrm{Fin2\text{-}ofFin}(i\;\text{succ}) = \mathrm{fs}(\mathrm{Fin2\text{-}ofFin}(i)).$$$
Lean4
/-- Converts a `Fin` into a `Fin2`. -/
def ofFin {n : Nat} (i : Fin n) : Fin2 n :=
i.succRec (fun _ => fz) (fun _ _ => fs)
