Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-23 22:02 340d5a9d

View on Github →

refactor(geometry/manifold/*): rename to charted_space and tangent_map (#3103) @PatrickMassot had asked some time ago if what is currently called manifold in mathlib could be renamed to charted_space, and in a recent PR he asked if bundled_mfderiv could be called tangent_map. Both changes make sense. They are implemented in this PR, together with several tiny improvements to the manifold library.

Estimated changes

modified theorem equiv.refl_to_local_equiv
modified theorem equiv.symm_to_local_equiv
modified theorem equiv.to_local_equiv_coe
modified theorem equiv.to_local_equiv_source
modified theorem equiv.to_local_equiv_target
modified theorem equiv.trans_to_local_equiv
modified theorem local_equiv.coe_mk
modified theorem local_equiv.coe_symm_mk
modified theorem local_equiv.coe_trans
modified theorem local_equiv.coe_trans_symm
modified theorem local_equiv.inv_fun_as_coe
modified theorem local_equiv.left_inv
modified theorem local_equiv.map_source
modified theorem local_equiv.map_target
modified theorem local_equiv.of_set_coe
modified theorem local_equiv.of_set_source
modified theorem local_equiv.of_set_symm
modified theorem local_equiv.of_set_target
modified theorem local_equiv.prod_coe
modified theorem local_equiv.prod_coe_symm
modified theorem local_equiv.prod_source
added theorem local_equiv.prod_symm
modified theorem local_equiv.prod_target
added theorem local_equiv.prod_trans
modified theorem local_equiv.refl_coe
modified theorem local_equiv.refl_source
modified theorem local_equiv.refl_symm
modified theorem local_equiv.refl_target
modified theorem local_equiv.refl_trans
modified theorem local_equiv.restr_coe
modified theorem local_equiv.restr_coe_symm
modified theorem local_equiv.restr_source
modified theorem local_equiv.restr_target
modified theorem local_equiv.restr_univ
modified theorem local_equiv.right_inv
modified theorem local_equiv.symm_source
modified theorem local_equiv.symm_symm
modified theorem local_equiv.symm_target
modified theorem local_equiv.to_fun_as_coe
modified theorem local_equiv.trans_refl
modified theorem local_equiv.trans_source
modified theorem local_equiv.trans_target
modified theorem chart_at_model_space_eq
added structure charted_space_core
deleted theorem manifold_core.open_target
deleted structure manifold_core
added theorem mem_maximal_atlas_iff
modified theorem model_space_atlas
modified def structomorph.refl
deleted def bundle_mfderiv
deleted theorem bundle_mfderiv_chart
deleted theorem bundle_mfderiv_chart_symm
deleted theorem bundle_mfderiv_comp
deleted theorem bundle_mfderiv_comp_at
deleted theorem bundle_mfderiv_proj
modified theorem has_mfderiv_within_at_univ
modified theorem mfderiv_const
modified theorem mfderiv_id
modified theorem mfderiv_within_univ
added def tangent_map
added theorem tangent_map_chart
added theorem tangent_map_chart_symm
added theorem tangent_map_comp
added theorem tangent_map_comp_at
added theorem tangent_map_proj
added theorem unique_mdiff_on_univ
modified def ext_chart_at
modified theorem ext_chart_at_to_inv
modified theorem ext_chart_model_space_eq_id
modified theorem mem_ext_chart_source
modified theorem model_with_corners.left_inv
modified theorem model_with_corners.mk_coe
modified theorem model_with_corners.target
modified theorem model_with_corners_self_coe
modified theorem local_homeomorph.coe_coe
modified theorem local_homeomorph.coe_trans
modified theorem local_homeomorph.left_inv
modified theorem local_homeomorph.map_source
modified theorem local_homeomorph.map_target
modified theorem local_homeomorph.mk_coe
modified theorem local_homeomorph.of_set_coe
modified theorem local_homeomorph.prod_coe
modified theorem local_homeomorph.refl_coe
modified theorem local_homeomorph.refl_symm
modified theorem local_homeomorph.refl_trans
modified theorem local_homeomorph.restr_coe
modified theorem local_homeomorph.restr_univ
modified theorem local_homeomorph.right_inv
modified theorem local_homeomorph.symm_symm
modified theorem local_homeomorph.trans_refl