English
If a predicate P on the integers has a nonempty set of true values and is bounded above, then there exists a greatest integer ub with P(ub) and P(z) implies z ≤ ub for all z with P(z).
Русский
Если предикат P на целых числах имеет непустое множество истинных значений и ограничен сверху, тогда существует наибольшее целое ub такое, что P(ub) и P(z) → z ≤ ub для всех z с P(z).
LaTeX
$$$\forall P : \mathbb{Z} \to \mathrm{Prop},\ (\exists b : \mathbb{Z},\ \forall z : \mathbb{Z},\ P(z) \rightarrow z \le b) \land (\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
/-- If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded above and nonempty,
then this set has the greatest element. This lemma uses classical logic to avoid assumption
`[DecidablePred P]`. See `Int.greatestOfBdd` for a constructive counterpart. -/
theorem exists_greatest_of_bdd {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, P z → z ≤ b) (Hinh : ∃ z : ℤ, P z) :
∃ ub : ℤ, P ub ∧ ∀ z : ℤ, P z → z ≤ ub := by
classical
let ⟨b, Hb⟩ := Hbdd
let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
exact ⟨lb, H⟩
