rename `Inducing` and `Embedding`?

Stream: mathlib4

[Yury G. Kudryashov]

What do you think about renaming Inducing and Embedding to TopologyInducing and TopologyEmbedding, resp.?

[Yaël Dillies]

I agree they need to be renamed, but I disagree with your suggestion. Here's a list of my requests:

1. Make them be under the Topology namespace
2. Make it clear they are Prop-valued. Compare to docs#Function.Embedding which is Type-valued.

[Yury G. Kudryashov]

Or should I use IsTopologyInducing?

[Yaël Dillies]

Hence I would suggest Topology.IsInducing, Topology.IsEmbedding

[Yury G. Kudryashov]

We didn't use Topology as a namespace to be opened w/o scoped yet.

[Yury G. Kudryashov]

But probably we should (and move some stuff from TopologicalSpace NS)

[Yaël Dillies]

Yury G. Kudryashov said:

We didn't use Topology as a namespace to be opened w/o scoped yet.

Have we not? I thought we had already moved some things in that namespace

[Yury G. Kudryashov]

Possibly, I missed this.

[Patrick Massot]

As I already wrote several times, I'm in favor or namespacing those definitions. Their current status is a historical accident.

[Yury G. Kudryashov]

I started working on this, I hope to open a PR over the weekend.