English
If c is a Primrec predicate and f,g are Primrec, then the conditional function a ↦ if c a then f a else g a is Primrec.
Русский
Если c — Primrec предикат, а f и g — Primrec, то функция условного выбора f или g по c является Primrec.
LaTeX
$$$ PrimrecPred c \rightarrow Primrec f \rightarrow Primrec g \rightarrow Primrec (\\lambda a. if c a then f a else g a)$$$
Lean4
theorem cond {c : α → Bool} {f : α → σ} {g : α → σ} (hc : Primrec c) (hf : Primrec f) (hg : Primrec g) :
Primrec fun a => bif (c a) then (f a) else (g a) :=
(nat_casesOn (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq fun a => by cases c a <;> rfl
