vector_get'

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.vector_get'

English

The uncurried form of vector get is primitive recursive.

Русский

Неоднозначенная форма получения элемента вектора примитивно-рекурсивна.

LaTeX

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

Lean4

theorem vector_get' {n} : Primrec (@List.Vector.get α n) :=
  of_equiv_symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru