decide — Mathlib

English

If α and β are denumerable and σ is primcodable, then Primrec₂ f ↔ Primrec₂ (m,n) ↦ f(Denumerable.ofNat α m, Denumerable.ofNat β n).

Русский

Если α и β счётны, а σ примитивно кодируем, то Primrec₂ f эквивалентно Primrec₂( m,n ↦ f(Denumerable.ofNat α m, Denumerable.ofNat β n)).

LaTeX

$$$\operatorname{Primrec}_2 f \iff \operatorname{Primrec}_2 \bigl( (m,n) \mapsto f(\operatorname{Denumerable.ofNat} \alpha m, \operatorname{Denumerable.ofNat} \beta n) \bigr)$$$

Lean4

protected theorem decide {R : α → β → Prop} [DecidableRel R] (hR : PrimrecRel R) :
    Primrec₂ (fun a b => decide (R a b)) :=
  PrimrecPred.decide hR

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