vec_iff — Mathlib

English

A vector-valued function is primitive recursive iff its component function is primitive recursive.

Русский

Векторно-значимая функция примитивно рекурсивна тогда и только тогда, когда каждая её компонентная функция примитивно рекурсивна.

LaTeX

$$$\forall {m n} {f : List.Vector NAT m \to List.Vector NAT n},\ Nat.Primrec'.Vec f \leftrightarrow Primrec f$$$

Lean4

theorem vec_iff {m n f} : @Vec m n f ↔ Primrec f :=
  ⟨fun h => by simpa using Primrec.vector_ofFn fun i => to_prim (h i), fun h i =>
    of_prim <| Primrec.vector_get.comp h (.const i)⟩

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