isCofinal_empty_iff

Mathlib.Order.Cofinal

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

English

In a poset with a top element, IsCofinal s is equivalent to ⊤ ∈ s.

Русский

В частично упорядоченном множестве с верхним элементом IsCofinal s эквивалентно тому, что ⊤ ∈ s.

LaTeX

$$$IsCofinal s \iff \top \in s$$$

Lean4

theorem isCofinal_empty_iff : IsCofinal (∅ : Set α) ↔ IsEmpty α :=
  by
  refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty _⟩
  simpa using h a

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

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

Разделы

Аффилиация

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