vector_get — Mathlib

English

The function that returns the i-th element of a vector is primitive recursive.

Русский

Функция получения i-го элемента вектора примитивно-рекурсивна.

LaTeX

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

Lean4

theorem vector_get {n} : Primrec₂ (@List.Vector.get α n) :=
  option_some_iff.1 <|
    (list_getElem?.comp (vector_toList.comp fst) (fin_val.comp snd)).of_eq fun a => by simp [Vector.get_eq_get_toList]

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