Theorems · Theorem · logic and foundations

Partrec.recursiveIn

∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ} {O : Set (ℕ →. ℕ)},
  Partrec f → RecursiveIn O f

If a partial function is partial recursive, then it is RecursiveIn any oracle set.

Defined in

Mathlib.Computability.RecursiveIn

Cited by

6 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext

Assumes

PrimcodablePrimcodable