csSup_of_not_bddAbove

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

If s is not bounded above, then sSup s equals sSup of the empty set.

Русский

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

LaTeX

$$$ (hs : \neg BddAbove s) \Rightarrow sSup s = sSup \emptyset $$$

Lean4

@[simp]
theorem csSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup ∅ :=
  ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove s hs

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

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

Разделы

Аффилиация

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