nil

Mathlib.Computability.Primrec

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

English

For any n, the vector-valued function v ↦ List.Vector.nil is primitive recursive.

Русский

Для любого n векторная функция v ↦ List.Vector.nil является примитивно-рекурсивной.

LaTeX

$$$$ \\forall n, \\operatorname{Nat.Primrec'}\\big( \\lambda v : \\mathrm{List.Vector}\\ \\mathbb{N}\\ n, \\mathrm{List.Vector}.nil \\big). $$$$

Lean4

protected theorem nil {n} : @Vec n 0 fun _ => nil := fun i => i.elim0

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

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

Разделы

Аффилиация

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