Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-11 21:03 78065861

View on Github →

feat(analysis/calculus/deriv): extended API for derivatives (#1213)

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem differentiable.comp

deleted theorem differentiable.congr'

deleted theorem differentiable.congr

modified theorem differentiable.differentiable_on

deleted theorem differentiable_at.congr

added theorem differentiable_at.congr_of_mem_nhds

deleted theorem differentiable_at.fderiv_congr'

deleted theorem differentiable_at.fderiv_congr

modified theorem differentiable_on.mono

added theorem differentiable_within_at.congr_of_mem_nhds_within

deleted theorem differentiable_within_at.differentiable_at'

modified theorem differentiable_within_at.mono

modified theorem differentiable_within_at_inter

added theorem differentiable_within_at_univ

deleted theorem differentiable_within_univ_at

added theorem fderiv_congr_of_mem_nhds

added theorem fderiv_within_congr

added theorem fderiv_within_congr_of_mem_nhds_within

added theorem fderiv_within_inter

added theorem fderiv_within_subset

deleted theorem has_fderiv_at.congr

added theorem has_fderiv_at.congr_of_mem_nhds

modified theorem has_fderiv_at.fderiv

deleted theorem has_fderiv_at_congr

deleted theorem has_fderiv_at_filter.congr'

deleted theorem has_fderiv_at_filter.congr

added theorem has_fderiv_at_filter.congr_of_mem_sets

deleted theorem has_fderiv_at_filter_congr'

deleted theorem has_fderiv_at_filter_congr

added theorem has_fderiv_at_filter_congr_of_mem_sets

deleted theorem has_fderiv_within_at.congr

added theorem has_fderiv_within_at.congr_of_mem_nhds_within

modified theorem has_fderiv_within_at.fderiv_within

deleted theorem has_fderiv_within_at_congr

added theorem has_fderiv_within_at_inter'

added theorem has_fderiv_within_at_inter

added theorem has_fderiv_within_at_univ

deleted theorem has_fderiv_within_univ_at