English
The analytic groupoid is closed under restriction: restricting an analytic map to a smaller open set keeps it within the groupoid.
Русский
Аналитическая групоида замкнута относительно ограничения: если отображение аналитично на большем открытом множестве, то ограничение на меньшем открытом множестве также принадлежит групoid.
LaTeX
$$Instance: ClosedUnderRestriction (analyticGroupoid I)$$
Lean4
/-- An identity open partial homeomorphism belongs to the analytic groupoid. -/
theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) :
OpenPartialHomeomorph.ofSet s hs ∈ analyticGroupoid I :=
by
rw [analyticGroupoid, mem_groupoid_of_pregroupoid]
suffices h : AnalyticOn 𝕜 (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by simp [h, analyticPregroupoid]
have hi : AnalyticOn 𝕜 id (univ : Set E) := analyticOn_id
exact (hi.mono (subset_univ _)).congr (fun x hx ↦ I.right_inv hx.2)
