mathlib

646c035a - refactor(topology): mild reorganization (#1541)

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