sSup_empty

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#WithBot.sSup_empty

English

The supremum of the empty set in WithBot α is the bottom element.

Русский

Верхняя граница пустого множества в WithBot α равна нижнему элементу.

LaTeX

$$$$ \operatorname{sSup}(\emptyset) = \bot. $$$$

Lean4

@[simp]
theorem sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
  WithTop.sInf_empty (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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