Redefine `metrizable_space` etc

Stream: maths

[Yury G. Kudryashov]

Hi, I suggest the following refactor (depends on #14052).

1. Redefine pseudo_metrizable_space as "there exists a uniform space structure with countably generated uniformity that is compatible with the topology".
2. Redefine metrizable_space as pseudo_metrizable_space + t0_space. To avoid loops, the constructor will not be an instance.
3. Upgrade the instance [metrizable_space X] : t2_space X to [metrizable_space X] : regular_space X.
4. Define the instance [uniform_space X] [is_countably_generated (uniformity X)] : pseudo_metrizable_space X; it automatically covers pseudo_emetric_spaces.
5. Define the instance [uniform_space X] [is_countably_generated (uniformity X)] [separated_space X] : metrizable_space X. It automatically covers emetric_spaces. Note that we require [separated_space X] instead of [t0_space X] to avoid a loop.
6. Add a trivial definition pseudo_metrizable_space.to_uniform_space and lemmas pseudo_metrizable_space.is_countably_generated, pseudo_metrizable_space.separated_space.
7. If a lemma assumes that X is a uniform space with countably generated uniformity, then uses only the topological space structure, make it assume [pseudo_metrizable_space X] instead.
8. Move definitions of (pseudo_)(e)metric_spaces to a new file topology.metric_space.defs.
9. Put the contents of #14052 (reformulated to define pseudo_metrizable_space_pseudo_metric and metrizable_space_metric) between topology.metric_space.defs and topology.metric_space.emetric_space.
10. Similar to 7, but for (pseudo_)(e)metric_spaces.

What do you think?

[Sebastien Gouezel]

I had the impression that the point you had set up things before is that, when you have a uniform structure with countably generated uniformity, then you could generate a pseudometric whose uniformity was defeq to the original one. Isn't it something you would lose with this new implementation? (Personally I wouldn't really mind, because I never use the uniform structures -- maybe it would be enough to have this as a specific constructor, but not as an instance).

Setting this aside, I like the refactor you suggest, because I found it weird before that pseudo_metrizable_space only made sense for uniform spaces.

[Yury G. Kudryashov]

I'm going to leave uniform_space.to_pseudo_metric_space and uniform_space.to_metric_space. Then I'll define, e.g., pseudo_metrizable_space_pseudo_metric as @uniform_space.to_pseudo_metric_space _ pseudo_metrizable_space.to_uniform_space pseudo_metrizable_space.is_countably_generated_uniformity

[Yury G. Kudryashov]

This way all these definitions will be compatible with each other.

[Yury G. Kudryashov]

Once this refactor is done, I'm going to do a similar change to Polish spaces.