mathlib3

5936f530 - feat(topology/maps): for a continuous open map, preimage and interior commute (#9471)