instIsSimpleOrderOfNonemptyOfSubsingleton

English

If α is nonempty and has only one element (a singleton space), then the lattice of open sets is a two-element chain: {∅, α}.

Русский

Если пространство имеет один элемент, то множество открытых подмножеств образует двухэлементную цепь: ∅ и всё пространство.

LaTeX

$$$|\alpha| = 1 \text{ and } \alpha \neq \varnothing \quad\Rightarrow\quad \operatorname{Opens}(\alpha) = \{\varnothing, \alpha\}$$$

Lean4

instance [Nonempty α] [Subsingleton α] : IsSimpleOrder (Opens α) where
  eq_bot_or_eq_top := eq_bot_or_top <| Subsingleton.elim _ _

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