primrecPred_iff_primrec_decide — Mathlib

English

Primrec₂ of encoding is equivalent to Primrec₂ of the original function: Primrec₂ fun a b => encode(f(a,b)) ⇔ Primrec₂ f.

Русский

Primrec₂ кодирования эквивалентно Primrec₂ исходной функции: Primrec₂ (a,b) ↦ encode(f(a,b)) ⇔ Primrec₂ f.

LaTeX

$$$\bigl(\operatorname{Primrec}_2(\lambda a,b. \operatorname{encode}(f(a,b)))\bigr) \iff \operatorname{Primrec}_2 f$$$

Lean4

theorem primrecPred_iff_primrec_decide {p : α → Prop} [DecidablePred p] :
    PrimrecPred p ↔ Primrec (fun a => decide (p a))
    where
  mp := PrimrecPred.decide
  mpr := Primrec.primrecPred

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