English
Given n, there is a partial inverse from natural numbers to Fin2 n: optOfNat : ℕ → Option (Fin2 n), returning none if out of range, some finite index when in range.
Русский
Существуют частичные инверсии из ℕ в Fin2 n: optOfNat : ℕ → Option (Fin2 n), возвращает none, если число не попадает в диапазон, и some i, если попадает.
LaTeX
$$$\operatorname{optOfNat} : \mathbb{N} \to \mathrm{Option}(\mathrm{Fin2} n)$, с равенствами: \operatorname{optOfNat}(0) = \mathrm{none},\; \operatorname{optOfNat}(1) = \mathrm{some}\ fz,\; \operatorname{optOfNat}(n+1) = \mathrm{fs} \circ \operatorname{optOfNat}(n)$.$$
Lean4
/-- Converts a natural into a `Fin2` if it is in range -/
def optOfNat : ∀ {n}, ℕ → Option (Fin2 n)
| 0, _ => none
| succ _, 0 => some fz
| succ m, succ k => fs <$> @optOfNat m k
