Countable separating families of sets in topological spaces

In this file we show that a T₀ topological space with second countable topology has a countable family of open (or closed) sets separating the points.

instance instHasCountableSeparatingOnIsOpenOfT0SpaceOfSecondCountableTopologyElem {X : Type u_1} [TopologicalSpace X] {s : Set X} [T0Space ↑s] [SecondCountableTopology ↑s] : HasCountableSeparatingOn X IsOpen s

If X is a topological space, s is a set in X such that the induced topology is T₀ and is second countable, then there exists a countable family of open sets in X that separates points of s.

Equations

• ⋯ = ⋯

instance instHasCountableSeparatingOnIsClosedOfIsOpen {X : Type u_1} [TopologicalSpace X] {s : Set X} [h : HasCountableSeparatingOn X IsOpen s] : HasCountableSeparatingOn X IsClosed s

If there exists a countable family of open sets separating points of s, then there exists a countable family of closed sets separating points of s.

Equations

• ⋯ = ⋯