Splitting topology.v

[zstone1]

We've discussed at a handful of meetings that topology.v is too big at 8000 lines long. It causes at least 3 problems.

1. It makes it a pain to develop in topology.v because my IDE has to recheck 1000s of lines of boring stuff before I get to what I'm working on.
2. It makes imports of topology.v quite coarse, causing cyclic dependency annoyances.
3. Makes it hard to guess where existing results live, or new results should live

I propose an organization structure here that'll involve splitting into 4 files. Note that most of the complexity in splitting up the files lives in the middle. The function space topology stuff is easy to split off the end of the file. And the filter stuff should be easy to split off the beginning of the file. But the middle of the file is in "development order" not "theory order". For example, why is the subspace stuff at the end, but product stuff at the beginning? So I propose this as the final layout, and then we do 4, then 1, then the last split.

1. filters.v
   Basically just take all the filter stuff, and cut/paste it. It's mostly in the right order/organization now. But some later stuff should get moved in, such as ultra-filters.

2. topological_constructions.v

   I want to separate all these "basic" topological constructions to clean up the circular dependencies. None of the construction depend on anything more than continuity and filter stuff. This way I don't need to keep moving around results. For example, having to move "continuous_compact" at the end of the file because that's where subspace is defined.

   The first thing to define is continuity, and it's most basic properties. We don't want anything else in this file.

   Second, building topologies from other structures, and their relationship to continuity/convergence/open/closed.

   1. From basis (numDomainType)
   2. From subbasis
   3. Order topologies (ereals)
   4. Discrete topologies (bool)
   5. Cofinite topologies (nat)

   Third, building new topologies from old ones, and their relationships

   1. Product (just pairwise products, that is U * V)
   2. Subspace
   3. Weak, and particular, the subtype topology
   4. Quotient
   5. Sup

3. function_spaces.v

This is already drafted in #1166. It holds prod_topology, compact-open, uniform family.

4. topology.v

   For what remains, I'd like to reorganize it a bit to consolidate related lemmas some more. I'm also tempted to split out the separation axioms into their own file, so we can build their HB mixins in an nice isolated place. But I think we can declare success without that. If this file ends up being ~3000 lines it's still a big improvement from ~8000

[affeldt-aist]

NB: partly addressed by PR #1166, now merged