Commit 2024-11-02 14:17 2c07a25e

View on Github →

chore: expand fderiv API (#18512) Also rename _mono lemmas with an assumption (_ : s ∈ 𝓝[t] x) to mono_of_mem_nhdsWithin, and fderiv.comp (and friends) to fderiv_comp (and friends), as it is the current naming for mfderiv and it makes more sense since there is no possible dot notation here.

Estimated changes

deleted theorem derivWithin_of_mem
deleted theorem deriv.comp
deleted theorem deriv.comp_of_eq
deleted theorem derivWithin.comp
deleted theorem derivWithin.comp_of_eq
added theorem derivWithin_comp
added theorem derivWithin_comp_of_eq
added theorem deriv_comp
added theorem deriv_comp_of_eq
deleted theorem fderiv.comp_deriv
deleted theorem fderiv.comp_deriv_of_eq
added theorem fderiv_comp_deriv
added theorem fderivWithin_add'
added theorem fderivWithin_neg'
added theorem fderivWithin_sub'
added theorem fderiv_add'
added theorem fderiv_const_smul'
added theorem fderiv_neg'
added theorem fderiv_sub'
deleted theorem fderivWithin_of_mem
deleted theorem fderiv.comp
deleted theorem fderiv.comp_fderivWithin
deleted theorem fderivWithin.comp
deleted theorem fderivWithin.comp₃
added theorem fderivWithin_comp'
added theorem fderivWithin_comp
added theorem fderivWithin_comp₃
added theorem fderiv_comp'
added theorem fderiv_comp