isCofinal_iff_top_mem

Mathlib.Order.Cofinal

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

English

IsCofinal s iff ⊤ ∈ s holds when there is a top element.

Русский

IsCofinal s эквивалентно ⊤ ∈ s при наличии верхнего элемента.

LaTeX

$$IsCofinal s ↔ ⊤ ∈ s$$

Lean4

@[simp]
theorem isCofinal_iff_top_mem [OrderTop α] {s : Set α} : IsCofinal s ↔ ⊤ ∈ s :=
  ⟨IsCofinal.top_mem, fun hs _ ↦ ⟨⊤, hs, le_top⟩⟩

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

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

Разделы

Аффилиация

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