English
Given a predicate P on the integers with a computable upper bound b such that whenever P(z) holds we have z ≤ b, and provided there exists at least one z with P(z), there exists a greatest integer ub with P(ub) and such that every z with P(z) satisfies z ≤ ub.
Русский
Пусть P — предикат на целых числах, существует верхняя граница b такая, что если P(z), то z ≤ b, и существует z с P(z). Тогда существует наибольшее целое ub такое, что P(ub) и для всех z, если P(z), то z ≤ ub.
LaTeX
$$$\forall P : \mathbb{Z} \to \mathrm{Prop} \, [\mathrm{DecidablePred} \ P] \, \exists b \in \mathbb{Z},\ (\forall z : \mathbb{Z},\ P(z) \rightarrow z \le b) \rightarrow (\exists z : \mathbb{Z},\ P(z)) \rightarrow \exists ub : \mathbb{Z},\ P(ub) \land \forall z : \mathbb{Z},\ P(z) \rightarrow z \le ub$$$
Lean4
/-- A computable version of `exists_greatest_of_bdd`: given a decidable predicate on the
integers, with an explicit upper bound and a proof that it is somewhere true, return
the greatest value for which the predicate is true. -/
def greatestOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → z ≤ b) (Hinh : ∃ z : ℤ, P z) :
{ ub : ℤ // P ub ∧ ∀ z : ℤ, P z → z ≤ ub } :=
have Hbdd' : ∀ z : ℤ, P (-z) → -b ≤ z := fun _ h => neg_le.1 (Hb _ h)
have Hinh' : ∃ z : ℤ, P (-z) :=
let ⟨elt, Helt⟩ := Hinh
⟨-elt, by rw [neg_neg]; exact Helt⟩
let ⟨lb, Plb, al⟩ := leastOfBdd (-b) Hbdd' Hinh'
⟨-lb, Plb, fun z h => le_neg.1 <| al _ <| by rwa [neg_neg]⟩
