An isolated point in a countable Baire space

MathlibAnnex.Topology.exists_isOpen_singleton

theorem

Applies the Baire property to the closed cover by singletons.

Statement

Let be a nonempty countable topological space which is and Baire. Then some point is isolated: its singleton is open.

The condition says that singletons are closed. No metric, completeness, compactness or Hausdorff assumption beyond is required.

At least one singleton is open; the conclusion does not say that every point is isolated.

A countable closed cover of a nonempty Baire space has a member with nonempty interior.

Proof steps

The property makes each closed. Since is countable,
is a countable closed cover. The Closed-cover Baire theorem with the singleton family applies because is nonempty and Baire.
It yields with . Choose in that interior. Since , , so . Thus
and equals its interior and is open.

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

In the source	Mathematical meaning
`[Nonempty X]`	The topological space has at least one point, needed for the nonempty closed-cover conclusion.
`[Countable X]`	The cover indexed by the points of is countable.
`[T1Space X]`	Every singleton is closed.
`[BaireSpace X]`	has the Baire property, so a countable closed cover of nonempty has a member with nonempty interior.
`∃ x : X, IsOpen ({x} : Set X)`	There exists a point whose one-point subset is open in the original topology of .

Exact content identity

Declaration: MathlibAnnex.Topology.exists_isOpen_singleton

Accepted content SHA-256: 9d782ad21ca411aeea9e8dbd1b5723af5d0076bdbe930bee816b22302c48d2df

Accepted source guide SHA-256: 60543435636d429b48476a7513c4b81fe0031b057ebf51012d26ed942c4b1c54

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73