More Uniform Spaces

[zstone1]

Motivation for this change

My medium term goal is to prove stuff about the cantor space. One important feature of the space is that it is metrizable. It is possible to build the metric directly, and I have done so in my draft. However, it's a lot of proof for something so special cased. Instead, it seems more profitable to prove a bunch of general-purpose theorems even if it require going on a bit of a journey.

This change contains

1. Weak topologies from uniform spaces are uniform
2. Supremums of uniform topologies are uniform

with the immediate applications:

• infinite products of uniform spaces are uniform.
• The topology of compact convergence is uniform.

Next steps are

3. A uniform spaces is pseudometrizable iff there's a countable base for its entourage (AKA second countable)
4. Topologies defined over a second-countable sub-basis are themselves second countable
5. That countable products of metric spaces are metrizable follows immediately.

One downside to this approach is that you get very little control over the actual distance function. However needing the exact metric is rare practice, so I'm not worried about this. One additional benefit the second-countable condition provides is independence of a choice of R : realType.

The proof of sup_ent_nbhs is rather unpleasant due to all the dependent pairs. But trying to eliminate the dependent pairs in sup_ent made things even worse. If someone sees an approach to clean this up, I'd be quite interested. Otherwise what's here seems ok.

Things done/to do

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries, only append new ones, be careful: merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• [x] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.