English
If G is closed under restriction, then restricting any chart e in the maximal atlas to an open set s yields a chart e.restr s still in the maximal atlas.
Русский
Если G замыкается на ограничение, то ограничение любого чарта e из максимального атласа до открытого множества s также принадлежит максимальному атласу.
LaTeX
$$[ClosedUnderRestriction G] \; e \in G.maximalAtlas M \land \text{IsOpen}(s) \Rightarrow e.restr s \in G.maximalAtlas M$$
Lean4
/-- If a structure groupoid `G` is closed under restriction, for any chart `e` in the maximal atlas,
the restriction `e.restr s` to an open set `s` is also in the maximal atlas. -/
theorem restr_mem_maximalAtlas [ClosedUnderRestriction G] {e : OpenPartialHomeomorph M H} (he : e ∈ G.maximalAtlas M)
{s : Set M} (hs : IsOpen s) : e.restr s ∈ G.maximalAtlas M := fun _e' he' ↦
⟨restr_mem_maximalAtlas_aux1 G he he' hs, restr_mem_maximalAtlas_aux2 G he he' hs⟩
