English
If a predicate P on integers is bounded below by some b and nonempty, then there exists lb with P(lb) and lb ≤ z for all z with P(z).
Русский
Если предикат P на целых ограничен снизу некоторым b и не пуст, то существует наименьшее lb с P(lb) и lb ≤ z для всех z с P(z).
LaTeX
$$$\\exists lb \\; (P(lb) \\land \\forall z \\,(P(z) \\rightarrow lb \\le z))$$$
Lean4
/-- If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded below and nonempty,
then this set has the least element. This lemma uses classical logic to avoid assumption
`[DecidablePred P]`. See `Int.leastOfBdd` for a constructive counterpart. -/
theorem exists_least_of_bdd {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, P z → b ≤ z) (Hinh : ∃ z : ℤ, P z) :
∃ lb : ℤ, P lb ∧ ∀ z : ℤ, P z → lb ≤ z := by
classical
let ⟨b, Hb⟩ := Hbdd
let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
exact ⟨lb, H⟩
