English
Given a decidable predicate p on natural numbers with a witness, Nat.find returns the least n with p(n).
Русский
Пусть p — декidable предикат на ℕ и имеется свидетельство; тогда Nat.find возвращает наименьшее n такое, что p(n).
LaTeX
$$$p(\\mathrm{Nat.find}(H)) \\land \\forall m < \\mathrm{Nat.find}(H), \\lnot p(m).$$$
Lean4
/-- If `p` is a (decidable) predicate on `ℕ` and `hp : ∃ (n : ℕ), p n` is a proof that
there exists some natural number satisfying `p`, then `Nat.find hp` is the
smallest natural number satisfying `p`. Note that `Nat.find` is protected,
meaning that you can't just write `find`, even if the `Nat` namespace is open.
The API for `Nat.find` is:
* `Nat.find_spec` is the proof that `Nat.find hp` satisfies `p`.
* `Nat.find_min` is the proof that if `m < Nat.find hp` then `m` does not satisfy `p`.
* `Nat.find_min'` is the proof that if `m` does satisfy `p` then `Nat.find hp ≤ m`.
-/
protected def find : ℕ :=
(Nat.findX H).1
