subsingleton_of_bot_eq_top

Mathlib.Order.BoundedOrder.Basic

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

English

If ⊥ = ⊤, then α is Subsingleton.

Русский

Если ⊥ = ⊤, то α является Subsingleton.

LaTeX

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

Lean4

theorem subsingleton_of_bot_eq_top (hα : (⊥ : α) = (⊤ : α)) : Subsingleton α :=
  subsingleton_of_top_le_bot (ge_of_eq hα)

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

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

Разделы

Аффилиация

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