Commit 2022-07-22 09:11 51891bef

feat(topology/maps): add 2 lemmas, open function (#15612)

• Add is_open_map.of_inverse and is_open_map.range_mem_nhds.
• Open namespace function, add _root_ before embedding here and there. One lemma comes from a recent presentation at Brown University, another one comes from the sphere eversion project.