English
If α and β are denumerable and σ is primcodable, then f is Primrec₂ iff the Nat-encoded version f( Denumerable.ofNat α m, Denumerable.ofNat β n ) is Primrec₂.
Русский
Если α и β счётны, а σ примитивно кодируем, то f является Primrec₂ тогда и только тогда, когда его Nat-кодированная версия f(Denumerable.ofNat α m, Denumerable.ofNat β n) является Primrec₂.
LaTeX
$$$\bigl(\operatorname{Primrec}_2 f\bigr) \iff \operatorname{Primrec}_2 \bigl( (m,n) \mapsto f(\operatorname{Denumerable.ofNat} \alpha m, \operatorname{Denumerable.ofNat} \beta n) \bigr)$$$
Lean4
theorem ofNat_iff {α β σ} [Denumerable α] [Denumerable β] [Primcodable σ] {f : α → β → σ} :
Primrec₂ f ↔ Primrec₂ fun m n : ℕ => f (ofNat α m) (ofNat β n) :=
(Primrec.ofNat_iff.trans <| by simp).trans unpaired
