Namespacing docs#Path

Stream: mathlib4

[Yaël Dillies]

I just saw docs#Path is in the root namespace. Can a topologist suggest a suitable namespace for this declaration?

[Eric Wieser]

Should they all move within the Topology namespace?

[Floris van Doorn]

Or the TopologicalSpace namespace? (Can we merge these two namespaces?)

[Yaël Dillies]

I think we should drop the TopologicalSpace namespace entirely, except for things related to TopologicalSpace as a structure (eg inf and sup of topologies).

[Yaël Dillies]

I would even be happy to rename TopologicalSpace to Topology because it's shorter, not more ambiguous and would solve this double namespace issue.

[Patrick Massot]

I think TopologicalSpace is consistent with how we name algebraic structures. On paper we write “Let G be a group”, or “Let X be a topological space”.

[Patrick Massot]

And of course I’m happy with namespacing Path. This word is clearly too generic to be in the root namespace. For instance graph theory probably also want it.