fin_val — Mathlib

English

For every n, the canonical embedding i ↦ (i : ℕ) from Fin(n) to ℕ is primitive recursive.

Русский

Для каждого натурального числа n каноническое вложение i ↦ (i) из Fin(n) в ℕ является примитивно-рекурсивной функцией.

LaTeX

$$$$ \\forall n, \\ \\operatorname{Primrec}\\big( i \\mapsto (i : \\mathbb{N}) : \\mathrm{Fin}(n) \\to \\mathbb{N} \\big). $$$$

Lean4

theorem fin_val {n} : Primrec (fun (i : Fin n) => (i : ℕ)) :=
  fin_val_iff.2 .id

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