subset_sInf_of_not_bddBelow

Mathlib.Order.CompleteLatticeIntervals

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

English

If t is not bounded below, its infimum is the default element.

Русский

Если t не ограничено снизу, инфиминум равен дефолтному элементу.

LaTeX

$$$$ \neg \operatorname{BddBelow}(t) \Rightarrow \operatorname{sInf}(t) = \text{default}. $$$$

Lean4

theorem subset_sInf_of_not_bddBelow [Inhabited s] {t : Set s} (ht : ¬BddBelow t) : sInf t = default := by
  simp [sInf, ht]

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

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

Разделы

Аффилиация

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