English
Let α be a conditionally complete linear order with the order topology. If s is a nonempty closed subset of α and s is bounded above, then s has a maximum, namely the supremum sSup(s), and this maximum lies in s. Equivalently, sSup(s) is the greatest element of s.
Русский
Пусть α – частично упорядоченное линейное множество с условной полнотой и топологией порядка. Если s ⊆ α замкнутое множество не пусто и ограничено сверху, то у s есть максимум, равный sup s, и этот максимум принадлежит s. Эквивалентно, sSup s является наибольшим элементом s.
LaTeX
$$$s \neq \varnothing \land IsClosed(s) \land BddAbove(s) \Rightarrow sSup(s) \in s \land \forall x \in s\, (x \le sSup(s)).$$$
Lean4
theorem isGreatest_csSup {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) : IsGreatest s (sSup s) :=
IsClosed.isLeast_csInf (α := αᵒᵈ) hc hs B
