isLUB_csSup' — Mathlib

English

If s is bounded above, then sSup s is the least upper bound of s (IsLUB s (sSup s)).

Русский

Если множество ограничено сверху, то наибольшая верхняя граница является наименьшей верхней границей: IsLUB s (sSup s).

LaTeX

$$$\text{BddAbove}(s) \Rightarrow \text{IsLUB}(s, sSup(s))$$$

Lean4

theorem isLUB_csSup' {s : Set α} (hs : BddAbove s) : IsLUB s (sSup s) :=
  by
  rcases eq_empty_or_nonempty s with (rfl | hne)
  · simp only [csSup_empty, isLUB_empty]
  · exact isLUB_csSup hne hs

Похожие утверждения