subsingleton_iff_bot_eq_top — Mathlib

English

In a bounded order, bot equals top if and only if the whole order is a Subsingleton.

Русский

В ограниченном порядке нижний элемент равен верхнему тогда и только тогда, когда весь порядок является Subsingleton.

LaTeX

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

Lean4

theorem subsingleton_iff_bot_eq_top : (⊥ : α) = (⊤ : α) ↔ Subsingleton α :=
  ⟨subsingleton_of_bot_eq_top, fun _ => Subsingleton.elim ⊥ ⊤⟩

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