csSup_eq_top_of_top_mem

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

If ⊤ belongs to s in an OrderTop lattice, then sSup s = ⊤.

Русский

Если ⊤ принадлежит множеству в порядке с верхней границей, то sSup s = ⊤.

LaTeX

$$$ [OrderTop \ α] (\top ∈ s) \Rightarrow sSup s = \top $$$

Lean4

theorem csSup_eq_top_of_top_mem [OrderTop α] {s : Set α} (hs : ⊤ ∈ s) : sSup s = ⊤ :=
  csInf_eq_bot_of_bot_mem (α := αᵒᵈ) hs

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

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

Разделы

Аффилиация

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