prim — Mathlib

English

If f is a Nat.Primrec'.Vec, then f is a Nat.Partrec'.Vec (i.e., a vector-valued primitive recursive function yields a partial recursive vector function).

Русский

Если f — примитивно вычислимая векторная функция, то она также частично вычислима как вектор.

LaTeX

$$$$\forall \{n,m,f\},\; \mathrm{Nat.Primrec'.Vec}(f) \Rightarrow \mathrm{Nat.Partrec'.Vec}(f).$$$$

Lean4

nonrec theorem prim {n m f} (hf : @Nat.Primrec'.Vec n m f) : Vec f := fun i => prim <| hf i

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