Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-16 15:00 1d1f3841

View on Github →

feat(analysis/calculus/dslope): define dslope (#11432)

Estimated changes

Created src/analysis/calculus/dslope.lean

added theorem continuous_at.of_dslope

added theorem continuous_at_dslope_of_ne

added theorem continuous_at_dslope_same

added theorem continuous_on.of_dslope

added theorem continuous_on_dslope

added theorem continuous_within_at.of_dslope

added theorem continuous_within_at_dslope_of_ne

added theorem differentiable_at.of_dslope

added theorem differentiable_at_dslope_of_ne

added theorem differentiable_on.of_dslope

added theorem differentiable_on_dslope_of_nmem

added theorem differentiable_within_at.of_dslope

added theorem differentiable_within_at_dslope_of_ne

added theorem dslope_eventually_eq_slope_of_ne

added theorem dslope_eventually_eq_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 eq_on_dslope_slope

added theorem eq_on_dslope_sub_smul

added theorem sub_smul_dslope