Commit 2024-08-22 06:36 7ed205ef

feat: Define AnalyticManifold as a charted space compatible with analyticGroupoid (#10853)

1. Change the definition of analyticGroupoid to mean analytic everywhere including on the boundary, using the recently added AnalyticWithinAt def.
2. Define AnalyticManifold as a charted space compatible with analyticGroupoid. In finite dimensions AnalyticManifold is equivalent to SmoothManifoldWithCorners, so an alternative option would be to leave this out and prove the necessary correspondence via Osgood's theorem. However, we don't have Osgood's theorem yet, and it's nice to have a version that works arbitrarily.