New distance structures on Pseudo(e)metricspaces

Stream: mathlib4

[Arav Bhattacharyya]

Hi everyone. We (@Yaël Dillies ) are adding a way to obtain new distance structures on pseudo(e)metricspaces (#29321) and deciding whether replaceDist should replace dist and edist at once. Is one way preferred? Originally we just replaced dist and @Jireh Loreaux suggests that it replaces both at the same time. Thanks

[Yaël Dillies]

Could we have someone tie-breaking here? This is not a very important issue, but it is blocking the whole effort of upstreaming Prokhorov's theorem.

[Antoine Chambert-Loir]

Can you (or @Jireh Loreaux ) summarize the options here? It seems that the MetricSpace induced an EMetricSpace, so if I understand things correctly, the modification of the distance should modify the edistance accordingly, but if I understand things correctly, this is also required by docs#PseudoMetricSpace.edist_dist

[Yury G. Kudryashov]

The new (e)distance is propositionally equal to the old one.

[Yury G. Kudryashov]

So, we can replace dist while leaving edist as is. OTOH, if we define a function that replaces both, then we can call it with dist or edist as one of the arguments to override only one of them.

[Yury G. Kudryashov]

I mean, the functions you add in the PR don't let me override edist in a metric space without changing dist. I don't know if it's ever needed though.

[Jireh Loreaux]

My thinking was: if you were replacing dist, you'd maybe want to replace edist too (in a way that may be less true if you want to replace only the topology and not the bornology), and even if you don't, as you said, it's easy to leave one as-is.

[Arav Bhattacharyya]

@Sébastien Gouëzel left a review in favour of option 1, and for clarity this bit of the PR has been moved to #31015