Theorems · Theorem · global analysis

hasGroupoid_of_pregroupoid

∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (PG : Pregroupoid H),
  (∀ {e e' : OpenPartialHomeomorph M H},
      e ∈ atlas H M → e' ∈ atlas H M → PG.property (↑(e.symm.trans e')) (e.symm.trans e').source) →
    HasGroupoid M PG.groupoid

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceChartedSpace