Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_open_map.range_mem_nhds

Modification history

2022-07-22 09:11
src/topology/maps.lean
feat(topology/maps): add 2 lemmas, `open function` (#15612) …
Added is_open_map.range_mem_nhdsView on Github →