Theorem local_homeomorph.map_nhds_eq

feat(topology/local_homeomorph): add `is_image`, `piecewise`, and `disjoint_union` (#6804) …

feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753) …