Does `metric_space` really belong in `topology` ?

Stream: maths

[Rémi Bottinelli]

That's mostly an idle question, but isn't it kind of a historical artifact to see metric spaces as pertaining to topology?
I'm thinking e.g. of:

• For median spaces, graphs, convexity and friends, I don't think topology plays any role.
• Same for anything "coarse-geometric".

[Johan Commelin]

Do you think it should have its own top-level dir? Or be a subdir of analysis? Or another suggestion?

[Rémi Bottinelli]

I'd have it in its own top level dir, in the sense that it's neither a subfield of analysis, nor of topology, in my mind.

[Rémi Bottinelli]

But maybe "subfield" is not actually the best organizing principle? I asked the question since given the port to mathlib4 (which I'd like to help with at some point), I was wondering if it might make sense to correct that while it's still feasible (if it really is still feasible _and_ reasonable).

[Kevin Buzzard]

The idea during the port is to change as little as possible. If a refactor is being considered then it should be either done in mathlib3 ASAP, or (once the rising tide has reached metric spaces) in both mathlib3 and mathlib4, or should wait until after the port is complete in hopefully a few months. The idea is that during the port mathlib3 and mathlib4 should not diverge at all

[Rémi Bottinelli]

Ah, that makes sense: the point is to make the port as "direct" as possible?