vector_cons — Mathlib

English

The operation that prepends an element to a vector is primitive recursive (binary operation on vectors).

Русский

Операция добавления элемента в начале вектора является примитивно-рекурсивной (бинарная операция над векторами).

LaTeX

$$$$ \\operatorname{Primrec}_2\\big( \\mathrm{List.Vector.cons}\\ \\alpha\\ n \\big). $$$$

Lean4

theorem vector_cons {n} : Primrec₂ (@List.Vector.cons α n) :=
  vector_toList_iff.1 <| by simpa using list_cons.comp fst (vector_toList_iff.2 snd)

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