singleton_hasGroupoid — Mathlib

English

As above for an open embedding, the singleton charted space carries HasGroupoid.

Русский

Как и ранее, единичное пространство чарта несет HasGroupoid.

LaTeX

$$Theorem: (singleton_charted_space_hasGroupoid)$$

Lean4

theorem singleton_hasGroupoid {f : α → H} (h : IsOpenEmbedding f) (G : StructureGroupoid H) [ClosedUnderRestriction G] :
    @HasGroupoid _ _ _ _ h.singletonChartedSpace G :=
  (h.toOpenPartialHomeomorph f).singleton_hasGroupoid (toOpenPartialHomeomorph_source _ _) G

Похожие утверждения