Vec — Mathlib

English

Vec(f) holds when all coordinate projections of the vector-valued function f are primitive recursive.

Русский

Vec(f) означает, что все координаты проекций вектор функция f примитивно-рекурсивны.

LaTeX

$$$$ \\mathrm{Vec}_{n,m}(f) \\;:\\; \\iff\\; \\forall i, \\ \\operatorname{Primrec}'(\\lambda v, (f(v))_i). $$$$

Lean4

/-- A function from vectors to vectors is primitive recursive when all of its projections are. -/
def Vec {n m} (f : List.Vector ℕ n → List.Vector ℕ m) : Prop :=
  ∀ i, Primrec' fun v => (f v).get i

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