Theorem hasFDerivWithinAt_of_subsingleton

Modification history

2026-02-04 14:37
Mathlib/Analysis/Calculus/FDeriv/Const.lean
feat: `differentiable_of_subsingleton` (#34831) …
Added hasFDerivWithinAt_of_subsingletonView on Github →