Commit 2025-06-18 09:36 bb38781a

View on Github →

chore: add fun_ variants for Fréchet derivative of addition and like (#25865) This follows the new convention explained at https://leanprover-community.github.io/contribute/naming.html#unexpanded-and-expanded-forms-of-functions

Estimated changes

added theorem Differentiable.fun_add
added theorem Differentiable.fun_neg
added theorem Differentiable.fun_sub
added theorem Differentiable.fun_sum
modified theorem Differentiable.neg
modified theorem DifferentiableAt.neg
modified theorem DifferentiableOn.neg
added theorem HasFDerivAt.fun_sum
modified theorem differentiableAt_neg_iff
modified theorem differentiableOn_neg_iff
modified theorem differentiable_neg_iff
deleted theorem fderivWithin_add'
deleted theorem fderivWithin_const_smul'
added theorem fderivWithin_fun_add
added theorem fderivWithin_fun_neg
added theorem fderivWithin_fun_sub
added theorem fderivWithin_fun_sum
deleted theorem fderivWithin_neg'
deleted theorem fderivWithin_sub'
deleted theorem fderiv_add'
deleted theorem fderiv_const_smul'
added theorem fderiv_fun_add
added theorem fderiv_fun_const_smul
added theorem fderiv_fun_neg
added theorem fderiv_fun_sub
added theorem fderiv_fun_sum
deleted theorem fderiv_neg'
modified theorem fderiv_neg
deleted theorem fderiv_sub'