Commit 2023-05-25 21:14 45384496

View on Github →

feat: weaken assumptions in lemmas about fderivWithin (#4330) This is a partial forward-port of leanprover-community/mathlib#19045. I only forward-ported 1 file that was already merged into master. I'll do some git history rewrites in pending PRs instead.

Estimated changes

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

deleted theorem DifferentiableWithinAt.antimono

modified theorem DifferentiableWithinAt.congr_mono

modified theorem Filter.EventuallyEq.fderivWithin_eq

modified theorem Filter.EventuallyEq.fderivWithin_eq_nhds

modified theorem Filter.EventuallyEq.fderiv_eq

added theorem Filter.EventuallyEq.fderiv_within'

deleted theorem HasFDerivWithinAt.antimono

modified theorem HasFDerivWithinAt.congr'

modified theorem HasFDerivWithinAt.congr

modified theorem HasFDerivWithinAt.congr_mono

modified theorem HasFDerivWithinAt.insert

added theorem differentiableWithinAt_congr_set'

added theorem differentiableWithinAt_congr_set

modified theorem fderivWithin_congr'

modified theorem fderivWithin_congr

added theorem fderivWithin_congr_set'

added theorem fderivWithin_congr_set

added theorem fderivWithin_eventually_congr_set'

added theorem fderivWithin_eventually_congr_set

modified theorem fderivWithin_inter

added theorem fderivWithin_of_mem

deleted theorem fderivWithin_subset'

modified theorem fderivWithin_univ

added theorem hasFDerivWithinAt_congr_set'

added theorem hasFDerivWithinAt_congr_set

added theorem hasFDerivWithinAt_diff_singleton

modified theorem hasFDerivWithinAt_insert

modified theorem support_fderiv_subset

added theorem tsupport_fderiv_subset