unpaired'

Mathlib.Computability.Primrec

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

English

For f: ℕ → ℕ → ℕ, Nat.Primrec(Nat.unpaired f) is equivalent to Primrec₂ f.

Русский

Для f: ℕ → ℕ → ℕ, Nat.Primrec(Nat.unpaired f) эквивалентно Primrec₂ f.

LaTeX

$$$\operatorname{Nat.Primrec}(\operatorname{Nat.unpaired} f) \iff \operatorname{Primrec}_2 f$$$

Lean4

theorem unpaired' {f : ℕ → ℕ → ℕ} : Nat.Primrec (Nat.unpaired f) ↔ Primrec₂ f :=
  Primrec.nat_iff.symm.trans unpaired

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

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

Разделы

Аффилиация

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