refactor(topology): mild reorganization

[rwbarton]

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.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[rwbarton]

In order to make this PR easier to review, I tended to err on the side of minimizing changes, even when it left some individual modules with slightly odd orderings of theorems or variables setups. Those can be fixed in independent PRs after this one.

[rwbarton]

Marking this WIP until I've finished checking that I haven't inadvertently broken anything.

[rwbarton]

After arranging for Pi.topological_space and sigma.topological_space to take their universe arguments in the same order as before, there are just some boring changes, namely:

• I removed a redundant argument from is_open_prod_iff' on purpose.
• I made an argument of the instance normal_space.regular_space explicit for convenience.
• The instances in topology.bases moved into namespace topological_space, so their names changed.
• compact_range, dense_embedding.subtype, and the second_countable_topology instance had some implicit/typeclass arguments reordered.