Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-08 21:44 4ece2ee4

View on Github →

feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv (#15523)

Define achart
Rename and reformulate mem_maximal_atlas_of_mem_atlas -> subset_maximal_atlas
Used to prove smoothness of mfderiv (that result still has to be generalized to mfderiv_within, so is not included yet)
From the sphere eversion project

Estimated changes

Modified src/geometry/manifold/charted_space.lean

added def achart

added theorem achart_def

added theorem achart_val

added theorem coe_achart

deleted theorem structure_groupoid.mem_maximal_atlas_of_mem_atlas

added theorem structure_groupoid.subset_maximal_atlas

Modified src/geometry/manifold/cont_mdiff.lean

added theorem cont_mdiff_at_iff_cont_mdiff_at_nhds

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem cont_diff_on_ext_coord_change

added theorem cont_diff_within_at_ext_coord_change

added theorem ext_chart_at_target

added theorem ext_chart_model_space_apply

modified theorem ext_chart_model_space_eq_id

added theorem ext_chart_preimage_mem_nhds'

added theorem ext_chart_self_apply

added theorem ext_chart_self_eq

added theorem ext_coord_change_source

added theorem model_with_corners.injective

deleted theorem smooth_manifold_with_corners.mem_maximal_atlas_of_mem_atlas

added theorem smooth_manifold_with_corners.subset_maximal_atlas

Modified src/geometry/manifold/tangent_bundle.lean