Theorems · Theorem · logic and foundations

Primrec.nat_findGreatest

∀ {α : Type u_1} [inst : Primcodable α] {f : α → ℕ} {p : α → ℕ → Prop} [inst_1 : DecidableRel p],
  Primrec f → PrimrecRel p → Primrec fun x => Nat.findGreatest (p x) (f x)

Defined in

Mathlib.Computability.Primrec.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

PrimcodableDecidableRel