Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-08 17:23 2bde21d1

View on Github →

feat(geometry/manifold/times_cont_mdiff): API for checking times_cont_mdiff (#5631) Two families of lemmas:

to be times_cont_mdiff, it suffices to be times_cont_mdiff after postcomposition with any chart of the target
projection notation to go from times_cont_diff (in a vector space) to times_cont_mdiff

Estimated changes

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem smooth_iff_target

added theorem smooth_on_iff_target

added theorem smooth_within_at_iff_target

added theorem times_cont_diff.times_cont_mdiff

added theorem times_cont_diff_at.times_cont_mdiff_at

added theorem times_cont_diff_on.times_cont_mdiff_on

added theorem times_cont_diff_within_at.times_cont_mdiff_within_at

added theorem times_cont_mdiff_iff_target

added theorem times_cont_mdiff_on_iff_target

added theorem times_cont_mdiff_within_at_iff_target