Theorem contDiffWithinAt_iff_contDiffOn_nhds

Modification history

2024-11-29 21:45

Mathlib/Analysis/Calculus/ContDiff/Defs.lean

feat: update the `ContDiff` definition to integrate analytic functions in the hierarchy (#17152) …

Modified contDiffWithinAt_iff_contDiffOn_nhds View on Github →

2024-10-31 06:53

Mathlib/Analysis/Calculus/ContDiff/Defs.lean

chore: cleanup `ContDiffWithinAt` API, to match the `ContinuousAt` API (#18447) …

Added contDiffWithinAt_iff_contDiffOn_nhds View on Github →