Draft: Urysohn's Lemma via uniformities

[zstone1]

Motivation for this change

I'm on a roll finding applications of countable_uniform_pseudoMetricType_mixin. Here, we prove urysohn's lemma (well, 90% of it). The only remaining detail is building distance functions from pseudometrics. But as discussed, doing that correctly requires some generic machinery.

The proof itself is, as far as I know, a new proof. Given two separated sets A B, we use the same general idea as the standard rational induction: iteratively splice in open sets between A and ~B to build a "smooth" nested chain of open sets. However, this proof does not build the continuous function directly. Instead we show that this splicing technique produces a uniformity. That entourage has a couple features

1. It is a countable uniformity, so generates a psuedometric (a distance function exists)
2. It is coarser than the original topology (the distance function is continuous)
3. It collapses A, so for x,y with A x /\ A y we have dist x y = 0
4. It similarly collapses B
5. It separates A and B, so if A x and B y then dist x y > 0.

All together, this shows that fun z => min (dist(x,z)) (dist (x,y)) / dist(x,y) is exactly what we want.

A few interesting things here. This proof is pretty useless in a textbook. It requires a lot of background on uniformities to work. Two big pieces are required:

• Most significantly, we use countable_uniform_pseudoMetricType_mixin. The proof of this is substantially harder than the textbook proof urysohn's lemma.
• We also need to introduce the "uniform covering" and "star-refinement" machinery.

Another interesting thing: the proof is not meaningfully faster than the standard proof. Proving continuity in the standard approach is roughly as hard as proving the star-refinement relationship. The main distinction of this proof technique is that it avoids some painful details about induction over the rationals, and rational embeddings in the reals. In fact, nothing about the rationals is required to prove this, or any of its dependencies. One key benefit is reducing dependencies across the code. The fewer facts about Q required in topology.v the happier we will all be.

Like the cantor set stuff, I'm gonna break this apart into smaller, more reviewable chunks.

1. Covering uniformities generate entourages
2. Subbases for covering uniformities
3. The star-refinement for normal sequences
4. The final construction of the uniform space

Things done/to do

• 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)
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[zstone1]

Closing in favor of #900. It's a superior proof. The only thing that could be salvageable from here is the stuff on star-refinement. But that should be done with HB anyway.