Move some topology stuff into a namespace

Stream: general

[Andrew Yang]

In #17113, @Yaël Dillies suggested that embedding should not live in the root namespace. This occured when I wanted to add generalizing maps as _root_.generalizing. They suggested that we should move all predicates on maps between topological spaces into a namespace (perhaps topological_space or topology?), which I agree would be better. What do people think?

[Patrick Massot]

Sure. The word "embedding" in particular is super overloaded in mathematics, there is no way general topology can claim it. It's just a historical accident that it sits in the root namespace.

[Anatole Dedecker]

That makes sense to me. I would prefer topology to topological_space like we have metric instead of metric_space

[Jireh Loreaux]

uh.... docs#metric_space?

[Anatole Dedecker]

The lemmas are mostly in the metric namespace

[Jireh Loreaux]

oh I see

[Anatole Dedecker]

I’m not suggesting to change docs#topological_space

[Jireh Loreaux]

Changing the namespace could be nice.

[Yaël Dillies]

I'll do that then.