Commit 2023-05-28 14:10 910d34b6

View on Github →

feat: port Analysis.Calculus.Deriv.Comp (#4436)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Deriv/Comp.lean

added theorem HasDerivAt.comp_hasDerivWithinAt

added theorem HasDerivAt.comp_hasFDerivAt

added theorem HasDerivAt.comp_hasFDerivWithinAt

added theorem HasDerivAt.scomp_hasDerivWithinAt

added theorem HasDerivAtFilter.comp

added theorem HasDerivAtFilter.comp_hasFDerivAtFilter

added theorem HasDerivAtFilter.scomp

added theorem HasDerivWithinAt.comp

added theorem HasDerivWithinAt.comp_hasFDerivWithinAt

added theorem HasDerivWithinAt.scomp_hasDerivAt

added theorem HasFDerivAt.comp_hasDerivAt

added theorem HasFDerivAt.comp_hasDerivWithinAt

added theorem HasFDerivWithinAt.comp_hasDerivWithinAt

added theorem HasStrictDerivAt.comp

added theorem HasStrictDerivAt.comp_hasStrictFDerivAt

added theorem HasStrictDerivAt.scomp

added theorem HasStrictFDerivAt.comp_hasStrictDerivAt

added theorem deriv.comp

added theorem deriv.scomp

added theorem derivWithin.comp

added theorem derivWithin.scomp

added theorem fderiv.comp_deriv

added theorem fderivWithin.comp_derivWithin