An isolated point in a countable Baire space

MathlibAnnex.Topology.exists_isOpen_singleton

theorem

Extracts an isolated point from a nonempty countable T1 Baire space.

Statement

Let X be nonempty, countable, T1 and Baire. At least one singleton {x} is open in X.

Assumptions

Let X be nonempty, countable, T1 and Baire.

Conclusion

At least one singleton {x} is open in X.

Proof route

T1 makes each singleton closed. The countable union of those closed singletons is X; Mathlib's Baire closed-cover lemma gives one with nonempty interior. Since that interior lies inside a singleton, the singleton is open.

Main citations

Lean source signature (exact)

theorem exists_isOpen_singleton [Nonempty X] [Countable X] [T1Space X]
    [BaireSpace X] : ∃ x : X, IsOpen ({x} : Set X)

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON