Set_of_Integers_Bounded_Above_by_Integer_has_Greatest_Element
Provedintegersnumber-theoryproofwiki
Let S be a nonempty subset of the integers that is bounded above. Then S has a greatest element.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Set_of_Integers_Bounded_Above_by_Integer_has_Greatest_Element (S : Set ℤ) (hne : S.Nonempty) (hbdd : BddAbove S) : ∃ s ∈ S, ∀ t ∈ S, t ≤ s := by sorry
Source