Commit 2023-05-22 18:33 18d81fbc

View on Github →

feat: port Analysis.Calculus.Fderiv.Add (#4211)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/FDeriv/Add.lean

added theorem Differentiable.add

added theorem Differentiable.add_const

added theorem Differentiable.const_add

added theorem Differentiable.const_smul

added theorem Differentiable.const_sub

added theorem Differentiable.neg

added theorem Differentiable.sub

added theorem Differentiable.sub_const

added theorem Differentiable.sum

added theorem DifferentiableAt.add

added theorem DifferentiableAt.add_const

added theorem DifferentiableAt.const_add

added theorem DifferentiableAt.const_smul

added theorem DifferentiableAt.const_sub

added theorem DifferentiableAt.neg

added theorem DifferentiableAt.sub

added theorem DifferentiableAt.sub_const

added theorem DifferentiableAt.sum

added theorem DifferentiableOn.add

added theorem DifferentiableOn.add_const

added theorem DifferentiableOn.const_add

added theorem DifferentiableOn.const_smul

added theorem DifferentiableOn.const_sub

added theorem DifferentiableOn.neg

added theorem DifferentiableOn.sub

added theorem DifferentiableOn.sub_const

added theorem DifferentiableOn.sum

added theorem DifferentiableWithinAt.add

added theorem DifferentiableWithinAt.add_const

added theorem DifferentiableWithinAt.const_add

added theorem DifferentiableWithinAt.const_smul

added theorem DifferentiableWithinAt.const_sub

added theorem DifferentiableWithinAt.neg

added theorem DifferentiableWithinAt.sub

added theorem DifferentiableWithinAt.sub_const

added theorem DifferentiableWithinAt.sum

added theorem HasFDerivAt.sum

added theorem HasFDerivAtFilter.add_const

added theorem HasFDerivAtFilter.const_add

added theorem HasFDerivAtFilter.const_smul

added theorem HasFDerivAtFilter.const_sub

added theorem HasFDerivAtFilter.neg

added theorem HasFDerivAtFilter.sub

added theorem HasFDerivAtFilter.sub_const

added theorem HasFDerivAtFilter.sum

added theorem HasFDerivWithinAt.sum

added theorem HasStrictFDerivAt.add_const

added theorem HasStrictFDerivAt.const_add

added theorem HasStrictFDerivAt.const_smul

added theorem HasStrictFDerivAt.const_sub

added theorem HasStrictFDerivAt.neg

added theorem HasStrictFDerivAt.sub

added theorem HasStrictFDerivAt.sub_const

added theorem HasStrictFDerivAt.sum

added theorem differentiableAt_add_const_iff

added theorem differentiableAt_const_add_iff

added theorem differentiableAt_const_sub_iff

added theorem differentiableAt_neg_iff

added theorem differentiableAt_sub_const_iff

added theorem differentiableOn_add_const_iff

added theorem differentiableOn_const_add_iff

added theorem differentiableOn_const_sub_iff

added theorem differentiableOn_neg_iff

added theorem differentiableOn_sub_const_iff

added theorem differentiableWithinAt_add_const_iff

added theorem differentiableWithinAt_const_add_iff

added theorem differentiableWithinAt_const_sub_iff

added theorem differentiableWithinAt_neg_iff

added theorem differentiableWithinAt_sub_const_iff

added theorem differentiable_add_const_iff

added theorem differentiable_const_add_iff

added theorem differentiable_const_sub_iff

added theorem differentiable_neg_iff

added theorem differentiable_sub_const_iff

added theorem fderivWithin_add

added theorem fderivWithin_add_const

added theorem fderivWithin_const_add

added theorem fderivWithin_const_smul

added theorem fderivWithin_const_sub

added theorem fderivWithin_neg

added theorem fderivWithin_sub

added theorem fderivWithin_sub_const

added theorem fderivWithin_sum

added theorem fderiv_add

added theorem fderiv_add_const

added theorem fderiv_const_add

added theorem fderiv_const_smul

added theorem fderiv_const_sub

added theorem fderiv_neg

added theorem fderiv_sub

added theorem fderiv_sub_const

added theorem fderiv_sum