subsingleton_of_top_le_bot

Mathlib.Order.BoundedOrder.Basic

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

← MathLib Explorer

English

If ⊤ ≤ ⊥ in a bounded order, then α is a Subsingleton.

Русский

Если верхний элемент не выше нижнего, то множество α является Subsingleton.

LaTeX

$$$(\top \le \bot) \Rightarrow Subsingleton \alpha$$$

Lean4

theorem subsingleton_of_top_le_bot (h : (⊤ : α) ≤ (⊥ : α)) : Subsingleton α :=
  ⟨fun _ _ => le_antisymm (le_trans le_top <| le_trans h bot_le) (le_trans le_top <| le_trans h bot_le)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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