Theorems · Theorem · logic and foundations

ComputablePred.ite

∀ {f₁ f₂ : ℕ → ℕ},
  Computable f₁ →
    Computable f₂ →
      ∀ {c : ℕ → Prop} [inst : DecidablePred c], ComputablePred c → Computable fun k => if c k then f₁ k else f₂ k

The computable functions are closed under if-then-else definitions with computable predicates.

Defined in

Mathlib.Computability.RE

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePred