Commit 2022-09-17 23:24 ba584a4c

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.