English
Given a predicate P on integers that is decidable, with a known lower bound b and a witness that some z satisfies P, there exists a least lb with P(lb) and lb ≤ z for all z with P(z).
Русский
Для предиката P на целых, допускающего решение, существующая нижняя граница и существование хотя бы одного z с P(z) гарантируют существование наименьшего lb с P(lb) и lb ≤ z для всех z с P(z).
LaTeX
$$$\\exists lb \\, (P(lb) \\\\land \\\\forall z \\, (P(z) \rightarrow lb \\\\le z))$ where lb is the least such element.$$
Lean4
/-- A computable version of `exists_least_of_bdd`: given a decidable predicate on the
integers, with an explicit lower bound and a proof that it is somewhere true, return
the least value for which the predicate is true. -/
def leastOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z) (Hinh : ∃ z : ℤ, P z) :
{ lb : ℤ // P lb ∧ ∀ z : ℤ, P z → lb ≤ z } :=
have EX : ∃ n : ℕ, P (b + n) :=
let ⟨elt, Helt⟩ := Hinh
match elt, le.dest (Hb _ Helt), Helt with
| _, ⟨n, rfl⟩, Hn => ⟨n, Hn⟩
⟨b + (Nat.find EX : ℤ), Nat.find_spec EX, fun z h =>
match z, le.dest (Hb _ h), h with
| _, ⟨_, rfl⟩, h => add_le_add_left (Int.ofNat_le.2 <| Nat.find_min' _ h) _⟩
