primrecRel_iff_primrec_decide — Mathlib

English

For any f: α × β → σ, Primrec₂ (Function.curry f) is equivalent to Primrec f.

Русский

Для любой f: α × β → σ, Primrec₂ (Function.curry f) эквивалентно Primrec f.

LaTeX

$$$\operatorname{Primrec}_2(\mathrm{Function.curry} f) \iff \operatorname{Primrec} f$$$

Lean4

theorem primrecRel_iff_primrec_decide {R : α → β → Prop} [DecidableRel R] :
    PrimrecRel R ↔ Primrec₂ (fun a b => decide (R a b))
    where
  mp := PrimrecRel.decide
  mpr := Primrec₂.primrecRel

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