Commit 2026-01-31 05:34 dffa0f21

View on Github →

feat(Analysis/Calculus/FDeriv/Basic): generalize to TVS (#34345) Note that now that Differentiable.continuous takes the [Module k E] [ContinuousSMul k E], fun_prop is no longer willing to apply it due to metavariables in the type when trying to synthesize ContinuousSMul. This happens exactly once in mathlib.

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

modified theorem DifferentiableWithinAt.of_finite

modified theorem DifferentiableWithinAt.of_subsingleton

modified theorem HasFDerivAt.lim

modified theorem HasFDerivWithinAt.of_finite

modified theorem HasFDerivWithinAt.of_notMem_closure

modified theorem HasFDerivWithinAt.of_not_accPt

modified theorem HasFDerivWithinAt.of_subsingleton

modified theorem differentiableWithinAt_insert

modified theorem differentiableWithinAt_insert_self

modified theorem fderivWithin_eq_fderiv

modified theorem fderivWithin_id'

modified theorem fderivWithin_id

modified theorem fderivWithin_of_mem_nhdsWithin

modified theorem fderivWithin_zero_of_notMem_closure

modified theorem fderivWithin_zero_of_not_accPt

modified theorem fderiv_eq

modified theorem fderiv_id'

modified theorem fderiv_id

modified theorem hasFDerivWithinAt_diff_singleton

modified theorem hasFDerivWithinAt_insert

Modified Mathlib/Analysis/SpecialFunctions/Sigmoid.lean

modified theorem continuous_sigmoid