Theorem ContDiffWithinAt.differentiable_within_at'

Modification history

2024-10-10 16:56
Mathlib/Analysis/Calculus/ContDiff/Defs.lean
chore: rename leftovers from the port (#17619)
Deleted ContDiffWithinAt.differentiable_within_at'View on Github →
2023-06-01 05:37
Mathlib/Analysis/Calculus/ContDiffDef.lean
feat: port Analysis.Calculus.ContDiffDef (#4256)
Added ContDiffWithinAt.differentiable_within_at'View on Github →