Commit 2019-10-12 20:07 646c035a

refactor(topology): mild reorganization (#1541)

• refactor(topology): mild reorganization Another attempt to increase cohesion of modules in topology. The old constructions module was starting to turn into a collection of miscellaneous results, and didn't actually contain any constructions themselves. The major changes are:
• constructions now contains the definitions of the product, subspace, ... topologies, which used to be in order. This means that theorems involving concepts from maps (e.g., embeddings) and constructions (e.g., products) are now in constructions, not maps.
• subset_properties and separation now import constructions rather than the other way around. This means that theorems like "a product of compact spaces is compact" are now in subset_properties, not constructions.
• homeomorph is split off into its own file, which was easy because it was at the end of constructions anyways.
• reorder universes in constructions
• move README.md to docs/theories/topology.md
• expand documentation of metric/uniform spaces slightly
• update pointers to docs/theories/topological_spaces.md