Commit 2023-06-05 05:02 ddef6f41

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.InverseDeriv (#4676)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean

added theorem Real.contDiffAt_arccos

added theorem Real.contDiffAt_arccos_iff

added theorem Real.contDiffAt_arcsin

added theorem Real.contDiffAt_arcsin_iff

added theorem Real.contDiffOn_arccos

added theorem Real.contDiffOn_arcsin

added theorem Real.deriv_arccos

added theorem Real.deriv_arcsin

added theorem Real.deriv_arcsin_aux

added theorem Real.differentiableAt_arccos

added theorem Real.differentiableAt_arcsin

added theorem Real.differentiableOn_arccos

added theorem Real.differentiableOn_arcsin

added theorem Real.differentiableWithinAt_arccos_Ici

added theorem Real.differentiableWithinAt_arccos_Iic

added theorem Real.differentiableWithinAt_arcsin_Ici

added theorem Real.differentiableWithinAt_arcsin_Iic

added theorem Real.hasDerivAt_arccos

added theorem Real.hasDerivAt_arcsin

added theorem Real.hasDerivWithinAt_arccos_Ici

added theorem Real.hasDerivWithinAt_arccos_Iic

added theorem Real.hasDerivWithinAt_arcsin_Ici

added theorem Real.hasDerivWithinAt_arcsin_Iic

added theorem Real.hasStrictDerivAt_arccos

added theorem Real.hasStrictDerivAt_arcsin