Theorems · Definition · logic and foundations

ComputableIn

{α : Type u_5} → {σ : Type u_6} → [Primcodable α] → [Primcodable σ] → Set (ℕ →. ℕ) → (α → σ) → Prop

A total function is computable in O if its constant lift is recursive in O.

Defined in

Mathlib.Computability.RecursiveIn

Cited by

11 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

PrimcodablePrimcodable