English
If a predicate p on natural numbers has a witness, then there exists a least natural number n with p(n) true; this is captured by the construction finding the smallest witness.
Русский
Если на множестве натуральных чисел задан предикат p и существует число n с p(n), то существует наименьшее такое число.
LaTeX
$$$\\exists n \\in \\mathbb{N}, p(n) \\land \\forall m < n, \\lnot p(m).$$$
Lean4
/-- Find the smallest `n` satisfying `p n`. Returns a subtype. -/
protected def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
@WellFounded.fix _ (fun k => (∀ n < k, ¬p n) → { n // p n ∧ ∀ m < n, ¬p m }) lbp (wf_lbp H)
(fun m IH al =>
if pm : p m then ⟨m, pm, al⟩
else
have : ∀ n ≤ m, ¬p n := fun n h => Or.elim (Nat.lt_or_eq_of_le h) (al n) fun e => by rw [e]; exact pm
IH _ ⟨rfl, this⟩ fun n h => this n <| Nat.le_of_succ_le_succ h)
0 fun _ h => absurd h (Nat.not_lt_zero _)
