Commit 2026-02-04 14:37 58f4dfcb

View on Github →

feat: differentiable_of_subsingleton (#34831) and move a lemma to a better location. From the path towards immersions, submanifolds and the regular value theorem.

Estimated changes

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

added theorem differentiableOn_empty

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

deleted theorem differentiableOn_empty

added theorem differentiable_of_subsingleton

added theorem hasFDerivWithinAt_of_subsingleton