English
Let p be a predicate on the natural numbers with a decidable truth value. If there exists an n such that p(n) holds, then the set {n ∈ ℕ : p(n)} has a least element, namely Nat.find hp.
Русский
Пусть p — предикат на натуральных числах с допускаемым решением. Если существует такое число n, что p(n) истинно, то множество {n ∈ ℕ : p(n)} имеет наименьший элемент, равный Nat.find hp.
LaTeX
$$$\operatorname{IsLeast}\{n \in \mathbb{N} : p(n)\}\left(\mathrm{Nat.find}\, hp\right)$$$
Lean4
/-- `Nat.find` is the minimum natural number satisfying a predicate `p`. -/
theorem isLeast_find {p : ℕ → Prop} [DecidablePred p] (hp : ∃ n, p n) : IsLeast {n | p n} (Nat.find hp) :=
⟨Nat.find_spec hp, fun _ ↦ Nat.find_min' hp⟩
