English
If f1 and f2 are computable functions from N to N, and c is a computable predicate (DecidablePred), then the function k ↦ if c(k) then f1(k) else f2(k) is computable.
Русский
Пусть f1 и f2 — вычислимые функции от ℕ к ℕ, а c — вычислимый предикат (DecidablePred). Тогда функция k ↦ если c(k) выполняется, тогда f1(k), иначе f2(k) является вычислимой.
LaTeX
$$$\forall f_1,f_2 : \mathbb{N} \to \mathbb{N},\; \mathrm{Computable}(f_1) \to \mathrm{Computable}(f_2) \to \\ \forall c : \mathbb{N} \to \mathrm{Prop},\; [\mathrm{DecidablePred}(c)] \; (\mathrm{ComputablePred}(c)) \to \mathrm{Computable}\Bigl(k \mapsto \text{if } c(k) \text{ then } f_1(k) \text{ else } f_2(k)\Bigr).$$
Lean4
/-- The computable functions are closed under if-then-else definitions
with computable predicates. -/
theorem ite {f₁ f₂ : ℕ → ℕ} (hf₁ : Computable f₁) (hf₂ : Computable f₂) {c : ℕ → Prop} [DecidablePred c]
(hc : ComputablePred c) : Computable fun k ↦ if c k then f₁ k else f₂ k := by
simpa [Bool.cond_decide] using hc.decide.cond hf₁ hf₂
