English
If each f_i is primitive recursive, then the function a ↦ List.ofFn (λ i, f_i a) is primitive recursive.
Русский
Если каждый f_i примитивно-рекурсивен, то функция a ↦ List.ofFn(λ i, f_i a) примитивно-рекурсивна.
LaTeX
$$$$ \\forall n, \\forall f:\\mathrm{Fin}(n) \\to \\alpha \\to \\sigma,\\ (\\forall i:\\mathrm{Fin}(n), \\operatorname{Primrec}(f(i))) \\rightarrow \\operatorname{Primrec}\\big( a \\mapsto \\mathrm{List.ofFn}(\\lambda i. f(i)\\,a) \\big). $$$$
Lean4
theorem list_ofFn : ∀ {n} {f : Fin n → α → σ}, (∀ i, Primrec (f i)) → Primrec fun a => List.ofFn fun i => f i a
| 0, _, _ => by simp only [List.ofFn_zero]; exact const []
| n + 1, f, hf => by simpa using list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)
