head

Mathlib.Computability.Primrec

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

English

For every n, the head of the nth Primrec' function is primitive recursive.

Русский

Для каждого n голова n-й функции Primrec' примитивно-рекурсивна.

LaTeX

$$$$ \\forall n, \\operatorname{Primrec'}( \\mathrm{List.Vector.head} ) $$$$

Lean4

theorem head {n : ℕ} : @Primrec' n.succ head :=
  (get 0).of_eq fun v => by simp [get_zero]

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

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

Разделы

Аффилиация

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