vector_ofFn — Mathlib

English

If each f_i is computable, then a ↦ List.Vector.ofFn (λ i, f_i a) is computable.

Русский

Если каждый f_i вычислим, то a ↦ List.Vector.ofFn (λ i, f_i a) вычислима.

LaTeX

$$$\forall n, \forall f: Fin(n) \to \alpha \to \sigma, (\forall i, \mathrm{Computable} (f i)) \Rightarrow \mathrm{Computable}\; (a \mapsto \mathrm{List.Vector}.ofFn (\lambda i. f i a))$$$

Lean4

theorem vector_ofFn {n} {f : Fin n → α → σ} (hf : ∀ i, Computable (f i)) :
    Computable fun a => List.Vector.ofFn fun i => f i a :=
  (Partrec.vector_mOfFn hf).of_eq fun a => by simp

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