csSup_eq_univ_of_not_bddAbove

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

← MathLib Explorer

English

If s is not bounded above, then sSup s equals sSup univ.

Русский

Если s не ограничено сверху, то sSup s равно sSup множества всех элементов.

LaTeX

$$$ (\neg BddAbove s) \Rightarrow sSup s = sSup univ $$$

Lean4

theorem csSup_eq_univ_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup univ :=
  by
  rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]
  contrapose! hs
  exact hs.mono (subset_univ _)

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

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

Разделы

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

Аффилиация

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