csSup_Ioo — Mathlib

English

Let α be a densely ordered ConditionallyComplete lattice. For any a < b in α, the supremum of the open interval (a, b) equals b.

Русский

Пусть α — плотно упорядоченная условно полная решетка. Для любых a < b в α, супремум открытого интервала (a, b) равен b.

LaTeX

$$$ (a < b) \Rightarrow \operatorname{sSup}(\mathrm{Ioo}(a,b)) = b $$$

Lean4

@[simp]
theorem csSup_Ioo [DenselyOrdered α] (h : a < b) : sSup (Ioo a b) = b :=
  (isLUB_Ioo h).csSup_eq (nonempty_Ioo.2 h)

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