English
A function f : α → Fin(n) → σ is primitive recursive iff its two-argument form is primitive recursive.
Русский
Функция f : α → Fin(n) → σ примитивно-рекурсивна тогда и только тогда, когда соответствующая двухаргументная форма примитивно-рекурсивна.
LaTeX
$$$$ \\forall n, \\forall f:\\alpha \\to \\mathrm{Fin}(n) \\to \\sigma,\\ \\operatorname{Primrec}(f) \\iff \\operatorname{Primrec}_2(f). $$$$
Lean4
theorem fin_curry {n} {f : α → Fin n → σ} : Primrec f ↔ Primrec₂ f :=
⟨fun h => fin_app.comp (h.comp fst) snd, fun h =>
(vector_get'.comp (vector_ofFn fun i => show Primrec fun a => f a i from h.comp .id (const i))).of_eq fun a => by
funext i; simp⟩
