English
Restriction lemmas for maximal atlas with subtype spaces.
Русский
Леммы ограничения для максимального атласа в пространствах-подтипах.
LaTeX
$$SubtypeRestr_mem_maximalAtlas$$
Lean4
/-- If a groupoid `G` is `ClosedUnderRestriction`, then an open subset of a space which is
`HasGroupoid G` is naturally `HasGroupoid G`. -/
protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G where
compatible := by
rintro e e' ⟨_, ⟨x, hc⟩, he⟩ ⟨_, ⟨x', hc'⟩, he'⟩
rw [hc.symm, mem_singleton_iff] at he
rw [hc'.symm, mem_singleton_iff] at he'
rw [he, he']
refine G.mem_of_eqOnSource ?_ (subtypeRestr_symm_trans_subtypeRestr (s := s) _ (chartAt H x) (chartAt H x'))
apply closedUnderRestriction'
· exact G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _)
· exact isOpen_inter_preimage_symm (chartAt _ _) s.2
