Topology on ennreal.

Note: this is different from the emetric_space topology. The emetric_space topology has is_open {⊤}, while this topology doesn't have singleton elements.

In an emetric ball, the distance between points is everywhere finite

Each ball in an extended metric space gives us a metric space, as the edist is everywhere finite.

Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.