completely regular spaces and locally compact implies uniform

[zstone1]

We already have proofs about curry/uncurry which require locally compact and uniform. One one hand, these results are critical for homotopy theory. One the other hand they are badly phrased because locally compact implies uniform. That is what we prove here.

We follow the traditional proof, which is in 6 stages (2 of which were already done)

• compact implies normal (we had compact implies regular, this is an easy extension)
• normal implies completely regular (urysohn's lemma. already done as normal_separatorP + uniform_separatorP)
• completely regular + hausdorff implies unformizable (via the construction of sup {(weak_topology f) | f : X -> R is continuous})
• when X is locally compact + hausdorff, its one point compactification is compact + hausdorff
• X embeds into its one point compactification (AKA X is in the weak topology from its OPC)
• weak topologies respect uniformity (already done)

However, it's non-forgetful to just globally assign a Uniform to X. (And is legitimately dangerous. The nats with the discrete topology is hausdorff + locally compact, and does not have a unique uniformity).

Instead we do something slightly more general, and formalize the "continuous functions into the reals" construction by with a type completely_regular_uniformity . So if you have a crsX : completely_regular_space X, then the type completely_regular_uniformity crsX is uniform and satisfies (completely_regular_uniformity crsX: topologicalType) = X. And coq is smart enough to exploit this equality, as seen in completely_regular_regular.

Then it is enough to prove locally_compact_completely_regular, which do via a local non-forgetful inheritance, so it's ok.

Checklist

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md

• [x] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

the change to uniform_completely_regular was not documented in the changelog (unless I messed up with my changelog fix)

also, one_point_nbhs does not seem to be documented

[affeldt-aist]

Should "one point" by written "one-point" in the documentation?

I was a bit suprised you chose to use "opc" as part of lemma identifiers that are exposed to the user. Is it because it is a common abbreviation? Otherwise, I would expect potential users to search lemmas using the substrings such as "one", "point", or "compact", and potentially miss. Granted, "one_point_compactification" is very long, maybe "one_point" only if "compactification" is immediately understood? (not sure at all)

[zstone1]

I think one-point is better than one point. But I can't explain why.

And I definitely should not have exposed opc. Nobody would know what that means without context. The construction is not used all that often, so a long name is not a big deal. If we really wanted we could have both: the official lemma has a long name and also have a notation which aliases it. But I think that's overkill.

[affeldt-aist]

What about disabling the implicit parameter of normal_space and regular_space so that we are forces to write and see, say, normal_space T instead of just normal_space? This could make for better looking statements (e.g., completely_regular_regular) imo, it would correspond better to the documentation and the presentation of the various Ti might look more uniform.

[zstone1]

I think we did make that change, and just never went back and removed al the extra @s. We have

Arguments normal_space : clear implicits.
Arguments regular_space : clear implicits.

Removing the @s is an easy follow up PR I can do one this merges.

[affeldt-aist]

But instead of adding

Arguments normal_space : clear implicits.
Arguments regular_space : clear implicits.

you could also define normal_space and regular_space outside of the set_separations section:

Definition normal_space (T : topologicalType) :=
  forall A : set T, closed A ->
    filter_from (set_nbhs A) closure `=>` set_nbhs A.

Definition regular_space (T : topologicalType) :=
  forall a : T, filter_from (nbhs a) closure --> a.

to get the desired effect (then a user grepping the definitions will always found them fully applied as advertised in the header).