English
If each f_i is primitive recursive, then the vector-valued function a ↦ List.Vector.ofFn (λ i, f_i a) is primitive recursive.
Русский
Если каждый f_i примитивно-рекурсивен, то функция векторного значения a ↦ List.Vector.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.Vector.ofFn}(\\lambda i. f(i)\\,a) \\big). $$$$
Lean4
theorem vector_ofFn {n} {f : Fin n → α → σ} (hf : ∀ i, Primrec (f i)) :
Primrec fun a => List.Vector.ofFn fun i => f i a :=
vector_toList_iff.1 <| by simp [list_ofFn hf]
