nat_casesOn' — Mathlib

English

If f is Primrec and g is Primrec₂, then the function a ↦ (n.casesOn (f a) (g a)) is Primrec₂.

Русский

Если f примитивно рекурсивна, а g — Primrec₂, тогда функция a ↦ (n.casesOn (f a) (g a)) является Primrec₂.

LaTeX

$$$ Primrec f \rightarrow Primrec_2 g \rightarrow Primrec_2 (\\lambda a (n : \mathbb{N}). (n.casesOn (f a) (g a) : \beta))$$$

Lean4

theorem nat_casesOn' {f : α → β} {g : α → ℕ → β} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec₂ fun a (n : ℕ) => (n.casesOn (f a) (g a) : β) :=
  nat_rec hf <| hg.comp₂ Primrec₂.left <| comp₂ fst Primrec₂.right

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