mathlib

4ef4fefe - feat(geometry/manifold/cont_mdiff): more flexibility in changing charts (#15519)

feat(geometry/manifold/cont_mdiff): more flexibility in changing charts (#15519) * Adds lemmas that allows one to change the chart one considers for only the source or target * Also adds a lemma that shows `cont_mdiff_on` if the source and target lie completely in one chart. * Also add various properties for `local_invariant_prop` * From the sphere eversion project