Commit 2021-01-15 10:58 ed0ae3e7

View on Github →

feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753) More generally, the same is true for a map that is a local homeomorphism near every point.

Estimated changes

Modified src/analysis/calculus/inverse.lean

added theorem has_strict_deriv_at.map_nhds_eq

added theorem has_strict_fderiv_at.map_nhds_eq

added theorem open_map_of_strict_deriv

added theorem open_map_of_strict_fderiv

Modified src/order/filter/basic.lean

modified theorem filter.le_map

added theorem filter.le_map_of_right_inverse

added theorem filter.map_id'

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.map_nhds_eq

Modified src/topology/maps.lean

modified theorem is_open_map.image_mem_nhds

modified theorem is_open_map.is_open_range

modified theorem is_open_map.nhds_le

added theorem is_open_map.of_nhds_le