sumInl

Mathlib.Computability.Primrec

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

English

Sum.inl is primitive recursive.

Русский

Sum.inl является примитивно вычисимой.

LaTeX

$$$\\mathrm{Sum.inl}:\\alpha\\to(\\alpha\\oplus\\beta)$ is primitive recursive.$$

Lean4

theorem sumInl : Primrec (@Sum.inl α β) :=
  encode_iff.1 <| nat_double.comp Primrec.encode

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

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

Разделы

Аффилиация

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