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
instHasCountableSeparatingOnIsOpen
{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
instHasCountableSeparatingOnIsClosed
{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
- ⋯ = ⋯