English
For an open embedding f, the singleton charted space has HasGroupoid G.
Русский
Для открытого вложения f единичное пространство чарта имеет HasGroupoid G.
LaTeX
$$@HasGroupoid (\text{singletonChartedSpace of } f) G$$
Lean4
/-- Given an open partial homeomorphism `e` from a space `α` into `H`, if its source covers the
whole space `α`, then the induced charted space structure on `α` is `HasGroupoid G` for any
structure groupoid `G` which is closed under restrictions. -/
theorem singleton_hasGroupoid (h : e.source = Set.univ) (G : StructureGroupoid H) [ClosedUnderRestriction G] :
@HasGroupoid _ _ _ _ (e.singletonChartedSpace h) G :=
{ __ := e.singletonChartedSpace h
compatible := by
intro e' e'' he' he''
rw [e.singletonChartedSpace_mem_atlas_eq h e' he', e.singletonChartedSpace_mem_atlas_eq h e'' he'']
refine G.mem_of_eqOnSource ?_ e.symm_trans_self
have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption)
exact StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _) }
