English
An open partial homeomorphism f belongs to the analytic groupoid iff it and its inverse are analytic on the corresponding domains transported by I.
Русский
Отображение f принадлежит аналитической груподе тогда и только тогда, когда f и её обратное отображение аналитичны на соответствующих доменах, переносимых через I.
LaTeX
$$$f \\in \\mathrm{analyticGroupoid}(I) \\iff \\text{AnalyticOn } 𝕜(I \\circ f \\circ I^{-1}) (I^{-1}'s\\ domain) \\land \\text{AnalyticOn } 𝕜(I \\circ f^{-1} \\circ I^{-1}) (I^{-1}'s domain)$$$
Lean4
/-- Given a model with corners `(E, H)`, we define the groupoid of analytic transformations of
`H` as the maps that are `AnalyticOn` when read in `E` through `I`. Using `AnalyticOn`
rather than `AnalyticOnNhd` gives us meaningful definitions at boundary points. -/
@[deprecated "use instead `contDiffGroupoid ω`" (since := "2025-04-13")]
def analyticGroupoid : StructureGroupoid H :=
(analyticPregroupoid I).groupoid
