Commit 2025-04-30 09:03 819ba939

View on Github →

feat(FDeriv/Basic): add HasFDerivWithinAt.of_finite (#24466) ... and some corollaries

Estimated changes

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

added theorem DifferentiableWithinAt.of_finite

added theorem DifferentiableWithinAt.of_subsingleton

added theorem HasFDerivWithinAt.of_finite

added theorem HasFDerivWithinAt.of_subsingleton