Commit 2022-12-02 20:41 a1ce0bd9

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