unpaired — Mathlib

English

Unpairing a two-argument partial function preserves Partrec: Partrec f implies Partrec₂ (Nat.unpaired f) and conversely.

Русский

Разбиение пары в частично-рекурсивную функцию сохраняет Partrec: Partrec f эквивалентно Partrec₂ (Nat.unpaired f).

LaTeX

$$$\forall f:\gamma \to^. \delta,\ Partrec_2(f) \leftrightarrow Partrec(Nat.unpaired f).$$

Lean4

theorem unpaired {f : ℕ → ℕ →. α} : Partrec (Nat.unpaired f) ↔ Partrec₂ f :=
  ⟨fun h => by simpa using Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp, fun h =>
    h.comp Primrec.unpair.to_comp⟩

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