Commit 2023-11-07 14:27 430ef656

View on Github →

feat: lemmas analogous to fderiv_within_of_isOpen (#8057)

from the project towards Sard's theorem

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiffDef.lean

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

added theorem fderivWithin_of_isOpen

deleted theorem fderivWithin_of_open

added theorem hasFDerivWithinAt_of_isOpen

added theorem hasFDerivWithinAt_of_mem_nhds

Modified Mathlib/Geometry/Manifold/MFDeriv.lean

added theorem mfderivWithin_eq_mfderiv

added theorem mfderivWithin_of_isOpen

added theorem mfderivWithin_of_mem_nhds