chore(topology/constructions): deduplicate (#16505)
* rename `mem_closure_of_continuous` to `set.maps_to.closure_left`, move near `map_mem_closure`;
* merge `map_mem_closure2` and `mem_closure_of_continuous2` into `map_mem_closureâ‚‚`;
* fix&golf some proofs broken by these changes.
