Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-06 19:49 e6444585

View on Github →

feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts (#17668)

This PR generalizes some smoothness results from ext_chart_at to arbitrary members of the maximal atlas
Useful for smooth vector bundle refactor
Motivated by the sphere eversion project

Estimated changes

Modified src/geometry/manifold/cont_mdiff.lean

deleted theorem cont_diff_within_at_prop_mono

added theorem cont_diff_within_at_prop_mono_of_mem

added theorem cont_mdiff_at_extend

added theorem cont_mdiff_at_of_mem_maximal_atlas

added theorem cont_mdiff_at_symm_of_mem_maximal_atlas

added theorem cont_mdiff_model

added theorem cont_mdiff_on_iff_of_mem_maximal_atlas

added theorem cont_mdiff_on_iff_source_of_mem_maximal_atlas

added theorem cont_mdiff_within_at.mono_of_mem

added theorem cont_mdiff_within_at_congr_nhds

added theorem cont_mdiff_within_at_iff_image

added theorem cont_mdiff_within_at_iff_of_mem_maximal_atlas

modified theorem cont_mdiff_within_at_iff_of_mem_source

added theorem cont_mdiff_within_at_iff_source_of_mem_maximal_atlas

deleted theorem ext_chart_at_symm_continuous_within_at_comp_right_iff

deleted theorem model_with_corners.symm_continuous_within_at_comp_right_iff

Modified src/geometry/manifold/local_invariant_properties.lean

modified theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_iff

added theorem structure_groupoid.local_invariant_prop.lift_prop_within_at_mono_of_mem

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem local_homeomorph.extend_symm_continuous_within_at_comp_right_iff

added theorem model_with_corners.map_nhds_within_eq

added theorem model_with_corners.symm_continuous_within_at_comp_right_iff

added theorem model_with_corners.symm_map_nhds_within_image