Theorem AnalyticWithinAt.contDiffWithinAt
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) …
Added AnalyticWithinAt.contDiffWithinAtView on Github →2024-10-04 06:17
Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
feat: if a function is analytic on a set, its derivative also is, even if the space is not complete (#17221) …
Deleted AnalyticWithinAt.contDiffWithinAtView on Github →