Commit 2023-09-17 04:53 8b0612f6

View on Github →

feat: Add analytic structure groupoid on models with corners (#6386)

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem AnalyticAt.congr

added theorem AnalyticOn.congr'

added theorem AnalyticOn.congr

added theorem analyticAt_congr

added theorem analyticOn_congr'

added theorem analyticOn_congr

Modified Mathlib/Analysis/Analytic/Composition.lean

added theorem AnalyticOn.comp'

added theorem AnalyticOn.comp

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem hasGroupoid_inf_iff

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added def analyticGroupoid

added theorem mem_analyticGroupoid_of_boundaryless

added theorem ofSet_mem_analyticGroupoid

added theorem symm_trans_mem_analyticGroupoid