Mathlib Map

Theorems · Theorem · logic and foundations

Nat.RecursiveIn.subst

∀ {O O' : Set (ℕ →. ℕ)} {f : ℕ →. ℕ}, Nat.RecursiveIn O f → (∀ g ∈ O, Nat.RecursiveIn O' g) → Nat.RecursiveIn O' f

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

Defined in
Mathlib.Computability.RecursiveIn
Cited by
1 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

RecursiveIn.subst · cited by 2RecursiveIn.substSet · cited by 53352SetPFun · cited by 207PFunNat.RecursiveIn · cited by 8Nat.RecursiveInRecursiveIn.substCITED BYCITES

Cites3

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

  • Setstatement and proof · cited by 53,352
  • PFunstatement and proof · cited by 207
  • Nat.RecursiveInstatement and proof · cited by 8

Cited by1

Results whose statement or proof uses this declaration.