English
Let s be a nonempty subset of the integers that is bounded above by b. Then the supremum of s equals the greatest element of s not exceeding b, i.e. sSup s = greatestOfBdd b Hb Hinh.
Русский
Пусть s — непустое множество целых чисел, верхняя граница которого равна b. Тогда наибольший элемент множества, не превосходящий b, равен его верхнему пределу: sSup s = greatestOfBdd b Hb Hinh.
LaTeX
$$$\operatorname{sSup}(s) = \mathrm{greatestOfBdd}(b,\ Hb,\ Hinh)$$$
Lean4
theorem csSup_eq_greatest_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : ℤ) (Hb : ∀ z ∈ s, z ≤ b)
(Hinh : ∃ z : ℤ, z ∈ s) : sSup s = greatestOfBdd b Hb Hinh :=
by
have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
simp only [sSup, dif_pos this]
convert (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm
