primrecRel

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec₂.primrecRel

English

For any f: α × β → σ, Primrec(uncurry f) is equivalent to Primrec₂ f.

Русский

Для любой f: α × β → σ, Primrec(uncurry f) эквивалентно Primrec₂ f.

LaTeX

$$$\operatorname{Primrec}(\mathrm{Function.uncurry} f) \iff \operatorname{Primrec}_2 f$$$

Lean4

theorem primrecRel {R : α → β → Prop} [DecidableRel R] (hp : Primrec₂ (fun a b => decide (R a b))) : PrimrecRel R :=
  Primrec.primrecPred hp

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

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

Разделы

Аффилиация

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