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/Separation to this file.

instance TotallySeparatedSpace.t2Space {X : Type u_1} [TopologicalSpace X] [TotallySeparatedSpace X] : T2Space X

A totally separated space is T2.