subset_sSup_emptyset

Mathlib.Order.CompleteLatticeIntervals

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

English

The supremum of the empty subset of s is the default element.

Русский

Супремум пустого подмножества s равен дефолтному элементу.

LaTeX

$$$$ \operatorname{sSup}(\emptyset) = \text{default}. $$$$

Lean4

theorem subset_sSup_emptyset [Inhabited s] : sSup (∅ : Set s) = default := by simp [sSup]

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

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

Разделы

Аффилиация

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