toNat — Mathlib

English

Converts a Fin2 n into a natural number by the recursive rule: toNat(fz) = 0 and toNat(fs i) = succ(toNat i).

Русский

Переобразует Fin2 n в натуральное число так: toNat(fz) = 0 и toNat(fs i) = succ(toNat i).

LaTeX

$$$\text{toNat} : \forall \{n\}, \mathrm{Fin2}\,n \to \mathbb{N},\; \text{toNat}(\mathrm{fz}) = 0,\; \text{toNat}(\mathrm{fs}\ i) = \mathrm{succ}(\text{toNat}(i)).$$$

Lean4

/-- Converts a `Fin2` into a natural. -/
def toNat : ∀ {n}, Fin2 n → ℕ
  | _, @fz _ => 0
  | _, @fs _ i => succ (toNat i)

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