Set_of_Integers_Bounded_Below_by_Integer_has_Smallest_Element
Provedintegersproofwikiwell-ordering
Let S be a nonempty subset of the integers that is bounded below. Then S has a smallest element.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Set_of_Integers_Bounded_Below_by_Integer_has_Smallest_Element (S : Set ℤ) (hne : S.Nonempty) (hbdd : BddBelow S) : ∃ s ∈ S, ∀ t ∈ S, s ≤ t := by sorry
Source