nat_casesOn — Mathlib

English

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

Русский

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

LaTeX

$$$ Primrec f \rightarrow Primrec_2 g \rightarrow Primrec (\\lambda a. Nat.casesOn (f a) (g a))$$$

Lean4

theorem nat_casesOn {f : α → ℕ} {g : α → β} {h : α → ℕ → β} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
    Primrec fun a => ((f a).casesOn (g a) (h a) : β) :=
  (nat_casesOn' hg hh).comp .id hf

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