Mathlib Map

Theorems · Definition · logic and foundations

TuringReducible

(ℕ →. ℕ) → (ℕ →. ℕ) → Prop

f is Turing reducible to g if f is partial recursive given access to the oracle g

Defined in
Mathlib.Computability.TuringDegree
Cited by
6 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TuringEquivalent · cited by 4TuringEquivalentTuringReducible.partrec_of_const · cited by 1TuringReducible.partrec_o…TuringReducible.refl · cited by 1TuringReducible.reflPartrec.turingReducible · cited by 1Partrec.turingReducibleTuringReducible.rfl · cited by 0TuringReducible.rflTuringReducible.trans · cited by 0TuringReducible.transpartrec_iff_forall_turingReducible · cited by 0partrec_iff_forall_turing…TuringDegree · cited by 0TuringDegreePFun · cited by 207PFunRecursiveIn · cited by 15RecursiveInTuringReducibleCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by8

Results whose statement or proof uses this declaration.