Theorem DifferentiableWithinAt.of_subsingleton

Modification history

2026-01-31 05:34
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
feat(Analysis/Calculus/FDeriv/Basic): generalize to TVS (#34345) …
Modified DifferentiableWithinAt.of_subsingletonView on Github →
2025-04-30 09:03
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
feat(FDeriv/Basic): add `HasFDerivWithinAt.of_finite` (#24466) …
Added DifferentiableWithinAt.of_subsingletonView on Github →