Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 14:56 e85b152a

View on Github →

refactor(analysis/calculus/cont_diff): bit of cleanup (#17585)

  • Move some lemmas further down in the file (so that we can use more properties about cont_diff)
  • Rename cont_diff_clm_apply to cont_diff_clm_apply_iff
  • From the sphere eversion project
  • Part of #16946 (feel free to merge that PR directly instead of this one)

Estimated changes

added def cont_diff
modified def cont_diff_at
deleted theorem cont_diff_clm_apply
added def cont_diff_on
modified def cont_diff_within_at