English
If c, f, g are computable, then the conditional function a ↦ if c(a) then f(a) else g(a) is computable.
Русский
Если c, f и g вычислимы, то функция ветвления a ↦ если c(a) тогда f(a) иначе g(a) вычислима.
LaTeX
$$$\mathrm{Computable}\; c \to \mathrm{Computable}\; f \to \mathrm{Computable}\; g \Rightarrow \mathrm{Computable}\; (a \mapsto \mathrm{cond}\big(c(a), f(a), g(a)\big))$$$
Lean4
theorem cond {c : α → Bool} {f : α → σ} {g : α → σ} (hc : Computable c) (hf : Computable f) (hg : Computable g) :
Computable fun a => cond (c a) (f a) (g a) :=
(nat_casesOn (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq fun a => by cases c a <;> rfl
