fin_app — Mathlib

English

For every n, the evaluation map (v,i) ↦ v(i) is primitive recursive.

Русский

Для каждого n отображение оценки (v,i) ↦ v(i) является примитивно-рекурсивным.

LaTeX

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

Lean4

theorem fin_app {n} : Primrec₂ (@id (Fin n → σ)) :=
  (vector_get.comp (vector_ofFn'.comp fst) snd).of_eq fun ⟨v, i⟩ => by simp

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