Theorems · Theorem · logic and foundations

RecursiveIn.subst

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

If every element of O is RecursiveIn O', then any function which is RecursiveIn O is also RecursiveIn O'.

Defined in

Mathlib.Computability.RecursiveIn

Cited by

2 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

PrimcodablePrimcodable