mathlib3

c2368be5 - feat(topology/hom/open): Continuous open maps (#12406)

feat(topology/hom/open): Continuous open maps (#12406) Define `continuous_open_map`, the type of continuous opens maps between two topological spaces, and `continuous_open_map_class`, its companion hom class.