of_prim — Mathlib

English

If f is a partial recursive function on vectors (Partrec') and f equals g pointwise, then g is also Partrec'. In particular, equality transfer preserves partial recursiveness.

Русский

Если f частично рекурсивна для векторной функции и f равна g по точкам, тогда и g частично рекурсивна. Перенос равенства сохраняет частичную рекурсивность.

LaTeX

$$$$\forall \{n\} \{f,g : \mathrm{List.Vector} \mathbb{N} \ n \to \mathbb{N}\},\; \mathrm{Partrec'}(f) \to (\forall i, f(i)=g(i)) \to \mathrm{Partrec'}(g).$$$$

Lean4

theorem of_prim {n} {f : List.Vector ℕ n → ℕ} (hf : Primrec f) : @Partrec' n f :=
  prim (Nat.Primrec'.of_prim hf)

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