top_mem

Mathlib.Order.Cofinal

URI: https://scilib.ai/kg/mathlib#IsCofinal.top_mem

English

If s is cofinal, then ⊤ ∈ s.

Русский

Если s софинально, то ⊤ ∈ s.

LaTeX

$$IsCofinal s → ⊤ ∈ s$$

Lean4

theorem top_mem [OrderTop α] {s : Set α} (hs : IsCofinal s) : ⊤ ∈ s :=
  hs.mem_of_isMax isMax_top

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

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

Разделы

Аффилиация

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