Commit 2020-02-18 09:33 1435a196

View on Github →

refactor(topology/maps): split the proof of is_open_map_iff_nhds_le (#2007) Extract a lemma is_open_map.image_mem_nhds from the proof, and make the proof use this lemma.

Estimated changes

Modified src/topology/maps.lean

added theorem is_open_map.image_mem_nhds

modified def is_open_map

modified theorem is_open_map_iff_nhds_le