Separation and (dis)connectedness properties of topological spaces. #
This file provides an instance T2Space X given TotallySeparatedSpace X.
TODO #
- Move the last part of
Topology/Separationto this file.
instance
TotallySeparatedSpace.t2Space
{X : Type u_1}
[TopologicalSpace X]
[TotallySeparatedSpace X]
:
T2Space X
A totally separated space is T2.
Equations
- ⋯ = ⋯