list_ofFn — Mathlib

English

For any n, if each f_i is computable, then a ↦ List.ofFn (λ i, f_i a) is computable.

Русский

Для любого n, если каждый f_i вычислим, то a ↦ List.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}.ofFn (\lambda i. f i a))$$$

Lean4

theorem list_ofFn : ∀ {n} {f : Fin n → α → σ}, (∀ i, Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
  | 0, _, _ => by
    simp only [List.ofFn_zero]
    exact const []
  | n + 1, f, hf => by
    simp only [List.ofFn_succ]
    exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

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