Product embedding

[zstone1]

Motivation for this change

----- Overall goal ----- More cantor space helper theorems. The overall goal is to prove that, for countable I, I -> C is homeomorphic to C, where C is the cantor space. This is a result is as surprising as it is useful. For example, the existence of space filling curves for arbitrary dimensions becomes almost trivial. The overall approach is

1. Prove I -> C is totally disconnected, perfect, metrizable, and compact (I'm calling this combo of 4 properties cantor-like).
   • metrizable and compact following from tychonoff and #763, perfect and totally disconnected are pretty easy to prove
2. Prove that for every cantor-like T, it has a countable basis of clopen sets.
   • Proof is mostly done on a local branch. This is the tough part
3. The functions f_i = fun x => x \in A_i separate points from closed sets (where A_i is the countable basis of clopen sets)
   • this is rather easy
4. A family of functions that separate points from closed sets induces a embedding into a corresponding product.
   • This is what we prove in this PR
5. Lastly, we need to prove the induced embedding is surjective.
   • I think this has something to do with the "perfect set" property, but I'm not sure.

EDIT: on further reflection, surjectivity is trickier than I had originally realized. I'll need to think more carefully about this. It will involve some other more significant idea to make this embedding surjective. On the other hand, there seems to be no advantage to proving that I -> C is isomorphic to some subset of C.

----- This PR ----- We prove the "product embedding lemma" here.

1. What should the interface for this be? Should we expose a final theorem that says

exists (f : T -> PU), continuous f /\ open_map f /\ injective f?

The reason I didn't write this theorem it's sometimes useful to know that f(x)_i = f_i(x), such as proving surjectivity.

2. The main idea of the proof is to prove a bunch of topologies are equivalent. We don't have great machinery for this, and I assume HB will give us more. The proofs are fine as they are, but I do have to do some manual conversions between the topologies. It's certainly not a blocker.

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.