subset_sInf_emptyset

Mathlib.Order.CompleteLatticeIntervals

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

English

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

Русский

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

LaTeX

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

Lean4

theorem subset_sInf_emptyset [Inhabited s] : sInf (∅ : Set s) = default := by simp [sInf]

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

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

Разделы

Аффилиация

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