singletonChartedSpace_mem_atlas_eq

English

The singleton charted space inherits a HasGroupoid G from a structure groupoid G closed under restrictions.

Русский

Единичное пространство чарта наследует структуру HasGroupoid G из G, замкнутого на ограничения.

LaTeX

$$@HasGroupoid (domain) G$$

Lean4

theorem singletonChartedSpace_mem_atlas_eq (h : e.source = Set.univ) (e' : OpenPartialHomeomorph α H)
    (h' : e' ∈ (e.singletonChartedSpace h).atlas) : e' = e :=
  h'

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