Commit 2026-02-04 18:01 649a8ad4

View on Github →

feat(FDeriv/Congr): generalize to TVS (#34843)

Estimated changes

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

added theorem DifferentiableWithinAt.of_insert

added theorem HasFDerivWithinAt.of_insert

modified theorem HasFDerivWithinAt.of_notMem_closure

modified theorem HasFDerivWithinAt.of_not_accPt

modified theorem differentiableWithinAt_insert_self

modified theorem fderivWithin_zero_of_notMem_closure

modified theorem fderivWithin_zero_of_not_accPt

added theorem hasFDerivWithinAt_diff_singleton_self

added theorem hasFDerivWithinAt_insert_self

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

modified theorem DifferentiableWithinAt.fderivWithin_congr_mono

modified theorem differentiableWithinAt_congr_set'

added theorem differentiableWithinAt_congr_set_nhdsNE

modified theorem fderivWithin_congr_set'

added theorem fderivWithin_congr_set_nhdsNE

modified theorem fderivWithin_eventually_congr_set'

modified theorem hasFDerivWithinAt_congr_set'

added theorem hasFDerivWithinAt_congr_set_nhdsNE