Commit 2024-09-12 16:41 24f01798

chore: match the definition of AnalyticWithinAt with ContDiffWithinAt (#16725) The current definition of AnalyticWithinAt in a set s at a point x requires good behavior inside s, and continuity within s at x (because good behavior at x is important). In ContDiffWithinAt, where the issues are similar, one requires instead good behavior inside insert x s. Those two points of view are equivalent, but the latter is often more convenient (just one field to check, more uniform proofs). In this PR, we switch the definition of AnalyticWithinAt to the latter approach. We also expand a little bit the API around AnalyticWithinAt, by tweaking theorems that required AnalyticAt to require AnalyticWithinAt, and deduce AnalyticAt versions from AnalyticWithinAt versions. For this, a few statements have to be moved from the file Analytic.Within.lean to Analytic.Basic.lean. There is no real new statement or new proof in this PR, but it opens the way to further improvements.