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
- (_ : HasCountableSeparatingOn X IsOpen s) = (_ : HasCountableSeparatingOn X IsOpen s)
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
- (_ : HasCountableSeparatingOn X IsClosed s) = (_ : HasCountableSeparatingOn X IsClosed s)