mathlib

a1ce0bd9 - feat(geometry/manifold/smooth_manifold_with_corners): define local_homeomorph.extend (#17669)

feat(geometry/manifold/smooth_manifold_with_corners): define local_homeomorph.extend (#17669) * This generalizes the API of `ext_chart_at` to arbitrary local homeomorphisms * This allows us to generalize a bunch of properties of `ext_chart_at` (like smoothness) to arbitrary members of the atlas. * Fix some names: (primed versions are similarly renamed) ``` ext_chart_at_open_source -> is_open_ext_chart_at_source nhds_within_ext_chart_target_eq -> nhds_within_ext_chart_at_target_eq ext_chart_continuous_at_symm -> ext_chart_at_continuous_at_symm ext_chart_continuous_on_symm -> ext_chart_at_continuous_on_symm ext_chart_self_eq -> ext_chart_at_self_eq ext_chart_self_apply -> ext_chart_at_self_apply ext_chart_at_continuous_on -> continuous_on_ext_chart_at ext_chart_at_continuous_at -> continuous_at_ext_chart_at ext_chart_preimage_open_of_open -> is_open_ext_chart_at_preimage ext_chart_at_map_* -> map_ext_chart_at_* ext_chart_at_symm_map_* -> map_ext_chart_at_symm_* ext_chart_preimage_mem_nhds_within -> ext_chart_at_preimage_mem_nhds_within ext_chart_preimage_mem_nhds -> ext_chart_at_preimage_mem_nhds ext_chart_preimage_inter_eq -> ext_chart_at_preimage_inter_eq ext_chart_model_space_eq_id -> ext_chart_at_model_space_eq_id ext_chart_model_space_apply -> ext_chart_at_model_space_apply ``` * One notable unchanged (wrong) name is `mem_ext_chart_source`, but that should be renamed together with `mem_chart_source`. * Motivated by the sphere eversion project