unpaired'

Mathlib.Computability.Partrec

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

English

Equivalence between Nat.Partrec of Nat.unpaired and Partrec₂ f, for f: Nat → PFun Nat Nat.

Русский

Эквивалентность Nat.Partrec(Nat.unpaired f) и Partrec₂ f для f: Nat → PFun Nat Nat.

LaTeX

$$$\Partrec₂(f) \iff Nat.Partrec(Nat.unpaired f).$$

Lean4

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

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

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

Разделы

Аффилиация

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