Theorem AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn

Modification history

2024-11-27 09:04
Mathlib/Analysis/Analytic/Within.lean
chore: avoid importing `ContDiff.Defs` in `FDeriv.Analytic` (#19374) …
Added AnalyticWithinAt.exists_mem_nhdsWithin_analyticOnView on Github →