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 Countable products of metrics is metrizable #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

• 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.

[affeldt-aist]

Shouldn't weakT be a definition instead of a let?
When queried outside of the section, the statement of weak_sep_cvg
reveals the type of x as the unfolded version of weakT, which might be difficult to read.

[affeldt-aist]

During the course of a few proofs, there are goals that look obvious but that aren't because the relevant information
is in the type and is not displayed (e.g., F --> x -> F --> x in weak_sep_cvg).
The issue is not localized to the proof. When queried outside of the section, the statements of, e.g.,
weak_sep_nbhsE, weak_sep_openE, join_product_weak display trivial-looking equalities.
Don't we have any trick to have a better display?
Given how rich topology.v has become, we should maybe consider something to achieve disambiguation.
Maybe on the model of display's has used in order.v or for measure theory.

[zstone1]

goals that look obvious but that aren't

Yes, it's getting pretty bad. While proving things I find I am frequently switching "show notations", "show implicit arguments" and "show implicit conversions" off an on in vscode. It's pretty disruptive to the process.

Maybe on the model of display's has used in order.v or for measure theory.

Cyril mentioned something along these lines in #758. It sounds great. It seems like topology.v is due an overhaul sometime soon. I have some thoughts on the matter, but it makes sense for #698 to land first, rather than add in new ideas while also porting the old stuff.

[affeldt-aist]

goals that look obvious but that aren't

Yes, it's getting pretty bad. While proving things I find I am frequently switching "show notations", "show implicit arguments" and "show implicit conversions" off an on in vscode. It's pretty disruptive to the process.

I tried to add displays to the type of topologies so that open is displayed as d.-open for a topology of type topologicalType d.
You can observe the difference by looking at the lemma continuousP for example in
zstone1#2 .
I wanted to go as far as weak_sep_openE to see if we can make a difference but that won't be for today.
I am not sure whether it is necessary to propagate the display information up in the hierarchy until complete spaces, @CohenCyril ? (In which case, I might be stuck because of that.)

Maybe on the model of display's has used in order.v or for measure theory.

Cyril mentioned something along these lines in #758. It sounds great. It seems like topology.v is due an overhaul sometime soon. I have some thoughts on the matter, but it makes sense for #698 to land first, rather than add in new ideas while also porting the old stuff.

I was under the impression that the design of displays is mostly orthogonal to the strategy for packed classes (manual or HB) because the display information is essentially passed around without much fiddling. Moreover, I am not sure that displays will solve all the problems (is it the solution for a better display for filters? I don't know). So maybe it might be worth improving the situation at least for open and nbhs as soon as possible.

In any case, I draft-PRed my attempt so that it does not get lost.

[zstone1]

Also for this one, is it ready to go with the new notation?