English
The supremum is given by a branch depending on whether the set is nonempty and bounded above. If so, sSup s is the chosen least upper bound; otherwise it is defined to be 0.
Русский
Наибольшая верхняя грань множества определяется по признаку непустоты и ограниченности сверху: если таковое существует, берется наименьшая верхняя грань; иначе она равна 0.
LaTeX
$$$sSup(s) = \begin{cases} \text{the chosen } L & \text{if } s\neq\varnothing \wedge \mathrm{BddAbove}(s), \\ 0 & \text{otherwise} \end{cases}$$$
Lean4
theorem sSup_def (s : Set ℝ) :
sSup s = if h : s.Nonempty ∧ BddAbove s then Classical.choose (exists_isLUB h.1 h.2) else 0 :=
rfl
