last — Mathlib

English

The greatest value of Fin2 (n+1) is defined by last 0 = fz and last (n+1) = fs (last n).

Русский

Наибольшее значение Fin2 (n+1) задаётся как last 0 = fz; last (n+1) = fs (last n).

LaTeX

$$$\text{last} : \{n : \mathbb{N}\} \to \mathrm{Fin2}(n+1),\; \text{last}(0) = \mathrm{fz},\; \text{last}(n+1) = \mathrm{fs}(\text{last}(n))$$$

Lean4

/-- The greatest value of `Fin2 (n+1)`. -/
def last : {n : Nat} → Fin2 (n + 1)
  | 0 => fz
  | n + 1 => fs (@last n)

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