unpair

Mathlib.Computability.Partrec

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

English

Nat.unpair is computable.

Русский

Nat.unpair вычислима.

LaTeX

$$$\text{Computable } Nat.unpair$$$

Lean4

theorem unpair : Computable Nat.unpair :=
  Primrec.unpair.to_comp

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

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

Разделы

Аффилиация

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