csSup_Iio

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#csSup_Iio

← MathLib Explorer

English

The supremum of Iio(a) is a.

Русский

Наибольшая верхняя граница Iio(a) равна a.

LaTeX

$$$sSup(Iio(a)) = a$$$

Lean4

@[simp]
theorem csSup_Iio [NoMinOrder α] [DenselyOrdered α] : sSup (Iio a) = a :=
  csSup_eq_of_forall_le_of_forall_lt_exists_gt nonempty_Iio (fun _ => le_of_lt) fun w hw => by
    simpa [and_comm] using exists_between hw

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru