id

Mathlib.Computability.Primrec

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

English

Identity function on natural numbers is primitive recursive.

Русский

Функция тождества на натуральных числах является примитивно-рекурсивной.

LaTeX

$$$$\\text{Primrec}(\\mathrm{id}_{\\mathbb{N}}).$$$$

Lean4

protected theorem id : Nat.Primrec id :=
  (left.pair right).of_eq fun n => by simp

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

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

Разделы

Аффилиация

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