Commit 2023-08-01 08:16 69e7283b

View on Github →

feat: add more lemmas about derivatives and tsupport (#6228)

Estimated changes

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

added theorem HasFDerivAt.of_not_mem_tsupport

added theorem HasFDerivWithinAt.of_not_mem_tsupport

added theorem HasStrictFDerivAt.of_not_mem_tsupport

added theorem fderiv_of_not_mem_tsupport