sSup_univ

Mathlib.Data.Real.Archimedean

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

English

Let Set.univ be the set of all real numbers. Then its supremum is 0.

Русский

Пусть множество всех вещественных чисел есть множество вселенных; его наименьшая верхняя грань равна 0.

LaTeX

$$$\\operatorname{sSup}(Set.univ) = 0$$$

Lean4

theorem sSup_univ : sSup (@Set.univ ℝ) = 0 :=
  Real.sSup_of_not_bddAbove not_bddAbove_univ

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

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

Разделы

Аффилиация

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