# 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

- ⋯ = ⋯