unpaired — Mathlib

English

For any f: ℕ → ℕ → α, the unary function Nat.unpaired f is primitive recursive iff f is a two-argument primitive recursive function.

Русский

Для любой f: ℕ → ℕ → α функция Nat.unpaired f является примитивно вычислимой по одной переменной тогда и только тогда, когда f является примитивно вычислимой функцией по двум переменным.

LaTeX

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

Lean4

theorem unpaired {f : ℕ → ℕ → α} : Primrec (Nat.unpaired f) ↔ Primrec₂ f :=
  ⟨fun h => by simpa using h.comp natPair, fun h => h.comp Primrec.unpair⟩

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