Metric Spaces are Normal

[zstone1]

Motivation for this change

Finishing track A of #965, this makes Tietze's theorem applicable to R. We do 4 small things:

1. Normality has 3 sensible definitions. We prove this with a tfae. Here we incorporate the the traditional "separable by open sets" notion of normality.
2. We define regular_space, and prove some basic facts about it.
3. We prove that pseudometric spaces are normal
4. We "fix" the interface for tietze's lemma to assume normal_space X instead of explicitly ask that X has separators.

Finally, this will let us turn lusin's continuous partial functions into genuine bounded, R->R continuous functions. This fully unblocks track B.

One weird thing comes up, where the proof for normal_spaceP goes through the real numbers, but they don't show up in the lemma statement. This is an opportunity to use a particular instance of realType to get the useless {R : realType} out of the signature. Where is there a concrete instance of realType in the mathcomp analysis?

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

Indeed we can use an instance of realType to remove the R : realType parameter from the statement of normal_spaceP but this requires to move a section from Rstruct.v to avoid a circularity when loading files. Is it acceptable?

[zstone1]

Looks great, exactly what I was hoping for. It also explains why searching for instances failed. There's probably a better way to organize this, but let's wait until I can split Topology into multiple files.

[affeldt-aist]

Then we can maybe think of merging but open an issue right away to remember that we need a better solution for this snippet of code that moved from Rstruct.v to normedtype.v. NB: We are also using Rstruct.v in another project that relies on the real numbers from the standard library, I am wondering what are the implications of splitting this compatibility layer and how useful this compatibility layer will turn out to be (I believe more useful that the attention we have been given to it so far).

[zstone1]

Yeah, a good real arithmetic package, even without the topology/measure theory stuff, is quite useful. We should at least put an issue to be settled before next release. I'm skeptical about why Rstruct depends on normedType at all.

[affeldt-aist]

I'm skeptical about why Rstruct depends on normedType at all.

We should maybe clear that up before merging.

[zstone1]

We should maybe clear that up before merging.

Ok, it was just a proof of one rather trivial lemma that we're not using anywhere. I rewrote the proof to avoid dependency on normedType, and things all work now. Assuming this builds, I think we're in good shape to merge.

[zstone1]

@affeldt-aist Well, some of the builds are broken, but they are a curl timeout. I'm probably not responsible for that, so we should be able to merge this one.

[affeldt-aist]

This introduces a dependency with Rstruct.v in normedtype.v but it is a very localized use so I think that this is reasonable.

[CohenCyril]

Why a local lemma rather than a global one?

[zstone1]

I was just following the pattern of the other TFAE proofs like cvgryPnum

[CohenCyril]

Oh right! Indeed there is probably no legitimate use of the 1 <-> 2 correspondance, we can leave it as such (maybe we can add a doc as a justfication)

[affeldt-aist]

@affeldt-aist Well, some of the builds are broken, but they are a curl timeout. I'm probably not responsible for that

Indeed, the last CI run is as green as it can be.