Theorems · Theorem · logic and foundations

Computable.find

∀ {α : Type u_1} [inst : Primcodable α] {P : α → ℕ → Prop} [inst_1 : DecidableRel P],
  (ComputablePred fun p => P p.1 p.2) → ∀ (hP_ex : ∀ (x : α), ∃ n, P x n), Computable fun x => Nat.find ⋯

If P is computable, and if for every x there exists an n such that P x n holds, then the function mapping x to the minimal such n (using Nat.find) is computable. This formally bridges Partrec.rfind with total unbounded search.

Defined in

Mathlib.Computability.RE

Cited by

0 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PrimcodableDecidableRel