Commit 2022-03-14 08:31 c2368be5
View on Github →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.