English
For any set s of real numbers, IsLUB s x is equivalent to IsGLB of the negated set; in particular, the supremum exists for nonempty bounded above sets via negation.
Русский
Для множества действительных чисел s равенство IsLUB s x эквивалентно IsGLB у отрицания множества; следовательно, верхняя грань существует при помочи преобразования через отрицание.
LaTeX
$$$\forall s:\{\mathbb{R}\},\; IsLUB(s,x) \iff IsGLB(-s,-x)$$$
Lean4
/-- A nonempty, bounded below set of real numbers has a greatest lower bound. -/
theorem exists_isGLB (hne : s.Nonempty) (hbdd : BddBelow s) : ∃ x, IsGLB s x :=
by
have hne' : (-s).Nonempty := Set.nonempty_neg.mpr hne
have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hbdd
use -Classical.choose (Real.exists_isLUB hne' hbdd')
rw [← isLUB_neg]
exact Classical.choose_spec (Real.exists_isLUB hne' hbdd')
