Commit 2023-05-30 08:23 6e4598a6

View on Github →

feat: port Analysis.Calculus.Dslope (#4491)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Dslope.lean

added theorem ContinuousAt.of_dslope

added theorem ContinuousLinearMap.dslope_comp

added theorem ContinuousOn.of_dslope

added theorem ContinuousWithinAt.of_dslope

added theorem DifferentiableAt.of_dslope

added theorem DifferentiableOn.of_dslope

added theorem DifferentiableWithinAt.of_dslope

added theorem continuousAt_dslope_of_ne

added theorem continuousAt_dslope_same

added theorem continuousOn_dslope

added theorem continuousWithinAt_dslope_of_ne

added theorem differentiableAt_dslope_of_ne

added theorem differentiableOn_dslope_of_nmem

added theorem differentiableWithinAt_dslope_of_ne

added theorem dslope_eventuallyEq_slope_of_ne

added theorem dslope_eventuallyEq_slope_punctured_nhds

added theorem dslope_of_ne

added theorem dslope_same

added theorem dslope_sub_smul

added theorem dslope_sub_smul_of_ne

added theorem eqOn_dslope_slope

added theorem eqOn_dslope_sub_smul

added theorem sub_smul_dslope