singleton_top

Mathlib.Order.Cofinal

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

English

The singleton set {⊤} is cofinal in any ordered type with a top.

Русский

Одиночное множество {⊤} является софинальным в любом упорядоченном множстве с верхним элементом.

LaTeX

$$IsCofinal {\top}$$

Lean4

theorem singleton_top [OrderTop α] : IsCofinal {(⊤ : α)} := fun _ ↦ ⟨⊤, Set.mem_singleton _, le_top⟩

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

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

Разделы

Аффилиация

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