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.
