Discrete topology/metric type-alias

[SnirBroshi]

We now have WithTopology X ⊥ for the discrete topology, so we can add abbrev Topology.Discrete X := WithTopology X ⊥.

#Is there code for X? > DiscreteTopology over the reals @ 💬

#Is there code for X? > Discrete MetricSpace/EMetricSpace @ 💬

Existing PR for the metric