sSup_of_not_bddAbove

Mathlib.Data.Real.Archimedean

URI: https://scilib.ai/kg/mathlib#Real.sSup_of_not_bddAbove

English

If s is not bounded above, then sSup s = 0.

Русский

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

LaTeX

$$$(\forall s, ¬\mathrm{BddAbove}(s)) \Rightarrow sSup(s) = 0$$$

Lean4

theorem sSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = 0 :=
  dif_neg fun h => hs h.2

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

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

Разделы

Аффилиация

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