unpair

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.unpair

English

The unpairing function Nat.unpair is primitive recursive.

Русский

Функция Nat.unpair примрrec.

LaTeX

$$$$ \\mathrm{Primrec}(\\mathrm{Nat.unpair}) $$$$

Lean4

theorem unpair : Primrec Nat.unpair :=
  (pair (nat_iff.2 .left) (nat_iff.2 .right)).of_eq fun n => by simp

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

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

Разделы

Аффилиация

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