Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-16 21:43 a116025e

View on Github →

feat(geometry/manifold/mfderiv): more lemmas (#6679)

move section mfderiv_fderiv up, add aliases;
rename old unique_mdiff_on.unique_diff_on to unique_mdiff_on.unique_diff_on_target_inter;
add a section about continuous_linear_map;
more lemmas about model_with_corners;
add lemmas about ext_chart_at.

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem has_fderiv_within_at.congr'

Modified src/geometry/manifold/mfderiv.lean

added theorem continuous_linear_map.mfderiv_eq

added theorem continuous_linear_map.mfderiv_within_eq

added theorem has_mfderiv_at_ext_chart_at

added theorem has_mfderiv_at_iff_has_fderiv_at

added theorem has_mfderiv_within_at_ext_chart_at

added theorem has_mfderiv_within_at_iff_has_fderiv_within_at

added theorem local_homeomorph.mdifferentiable.ker_mfderiv_eq_bot

added theorem local_homeomorph.mdifferentiable.mfderiv_injective

added theorem local_homeomorph.mdifferentiable.range_mfderiv_eq_top

added theorem mdifferentiable_at_ext_chart_at

added theorem mdifferentiable_on_ext_chart_at

modified theorem mfderiv_eq_fderiv

modified theorem mfderiv_within_eq_fderiv_within

added theorem model_with_corners.has_mfderiv_within_at_symm

deleted theorem model_with_corners.mdifferentiable

modified theorem model_with_corners.mdifferentiable_on_symm

deleted theorem unique_mdiff_on.unique_diff_on

added theorem unique_mdiff_on.unique_diff_on_target_inter

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem model_with_corners.continuous_at_symm

added theorem model_with_corners.continuous_within_at_symm

Modified src/geometry/manifold/times_cont_mdiff.lean