Commit 2024-01-09 18:26 bdd7632e

View on Github →

chore(*): fix more names (#9593) Grep for ^[^#].*deriv_within and fix all occurrences.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

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

added theorem Filter.EventuallyEq.fderivWithin'

deleted theorem Filter.EventuallyEq.fderiv_within'

Modified Mathlib/Analysis/Calculus/Taylor.lean

added theorem hasDerivWithinAt_taylorWithinEval_at_Icc

deleted theorem has_deriv_within_taylorWithinEval_at_Icc

Modified Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

added theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable

deleted theorem MeasureTheory.integral_eq_of_has_deriv_within_at_off_countable