English
If a family of functions f_i : α →. σ is given where each f_i is partial-recursive, then the function a ↦ List.Vector.mOfFn (λ i, f_i a) is partial-recursive.
Русский
Если задано семейство функций f_i : α →. σ, и каждая f_i частично вычислима, то функция a ↦ List.Vector.mOfFn (λ i, f_i a) частично вычислима.
LaTeX
$$$\forall n\, \forall f : Fin(n) \to \mathcal{P}\,\alpha \to\sigma,\; (\forall i, \mathrm{Partrec}(f_i)) \Rightarrow \mathrm{Partrec}\bigl( a \mapsto \mathrm{List.Vector}.mOfFn (\lambda i. f_i(a)) \bigr)$$$
Lean4
theorem vector_mOfFn :
∀ {n} {f : Fin n → α →. σ}, (∀ i, Partrec (f i)) → Partrec fun a : α => Vector.mOfFn fun i => f i a
| 0, _, _ => const _
| n + 1, f, hf => by
simp only [Vector.mOfFn, pure_eq_some, bind_eq_bind]
exact
(hf 0).bind
(Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
(Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))
