Nontrivial example of emetric space

Stream: maths

[Artie Khovanov]

What are some nontrivial, concrete examples of an emetric space (that's not a metric space)? Mathlib doesn't appear to have any such instances.

[Edward van de Meent]

a nontrivial example might be Nat -> ZMod 2 with the hamming distance/metric

[Edward van de Meent]

here the distance is the size of the set of indices where two elements are different.

[Jireh Loreaux]

Hausdorff distance on closed sets is another.

[Antoine Chambert-Loir]

docs#EReal is yet another one, more trivial than the two examples already given.

[Yury G. Kudryashov]

We use a different topology on EReal though.

[Yury G. Kudryashov]

Any example of an EMetricSpace can be described as "the disjoint union of two or more MetricSpaces, with infinite extended distance between points in different components".

[Yury G. Kudryashov]

One more example: if you consider Lp norm as a distance on the space of all measurable functions without restricting to the L^p space, then you get an EMetricSpace.

[Yury G. Kudryashov]

The L^p space is the "finite distance" component of zero in this EMetricSpace.

[Junyan Xu]

We don't have the facts that ENat, ENNReal and EReal are CompactSpace?
(Edit: Oh I guess they follow from compactSpace_of_completeLinearOrder; indeed #synth finds them.)

[Eric Wieser]

Yury G. Kudryashov said:

Any example of an EMetricSpace can be described as "the disjoint union of two or more MetricSpaces, with infinite extended distance between points in different components".

Should we have this instance on Sum and Sigma and Option?

[Yury G. Kudryashov]

At least in some cases, we introduce a different metric on Sum and Sigma by setting the distance between two arbitrary points to be one. CC: @Sébastien Gouëzel