Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes