vector_ofFn'

Mathlib.Computability.Primrec

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

English

The function List.Vector.ofFn is primitive recursive.

Русский

Функция List.Vector.ofFn примитивно-рекурсивна.

LaTeX

$$$$ \\forall n, \\operatorname{Primrec} \\big( \\mathrm{List.Vector.ofFn} \\; \\alpha\\; n \\big). $$$$

Lean4

theorem vector_ofFn' {n} : Primrec (@List.Vector.ofFn α n) :=
  of_equiv

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

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

Разделы

Аффилиация

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