csSup_lowerBounds_range

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

← MathLib Explorer

English

If IsGreatest s a, then sSup s ∈ s.

Русский

Если a является наибольшим элементом s, то sSup s принадлежит s.

LaTeX

$$$IsGreatest(s, a) \rightarrow \mathrm{sSup}(s) \in s$$$

Lean4

theorem csSup_lowerBounds_range [Nonempty β] {f : β → α} (hf : BddBelow (range f)) :
    sSup (lowerBounds (range f)) = ⨅ i, f i :=
  csSup_lowerBounds_eq_csInf hf <| range_nonempty _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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