English
If c is a PrimrecPred with decidable predicate and f,g are Primrec, then the function a ↦ ite (c a) (f a) (g a) is Primrec.
Русский
Если c — PrimrecPred с разрешимым предикатом, а f и g — Primrec, то функция a ↦ ite (c a) (f a) (g a) является Primrec.
LaTeX
$$$ PrimrecPred c \rightarrow Primrec f \rightarrow Primrec g \rightarrow Primrec (\\lambda a. ite (c a) (f a) (g a))$$$
Lean4
theorem ite {c : α → Prop} [DecidablePred c] {f : α → σ} {g : α → σ} (hc : PrimrecPred c) (hf : Primrec f)
(hg : Primrec g) : Primrec fun a => if c a then f a else g a := by
simpa [Bool.cond_decide] using cond hc.decide hf hg
