hasGroupoid_of_pregroupoid — Mathlib

English

If a preg roupoid PG on H with a compatibility assumption for all atlas charts holds, then there is a HasGroupoid M PG.groupoid.

Русский

Если выполняется предположение совместимости для всех карт атласа в отношении прегруппоида PG, то существует HasGroupoid M PG.groupoid.

LaTeX

$$$HasGroupoid\ M\ PG.groupoid$ if \text{PG satisfies the compatibility condition on atlas charts}.$$

Lean4

theorem hasGroupoid_of_pregroupoid (PG : Pregroupoid H)
    (h :
      ∀ {e e' : OpenPartialHomeomorph M H},
        e ∈ atlas H M → e' ∈ atlas H M → PG.property (e.symm ≫ₕ e') (e.symm ≫ₕ e').source) :
    HasGroupoid M PG.groupoid :=
  ⟨fun he he' ↦ mem_groupoid_of_pregroupoid.mpr ⟨h he he', h he' he⟩⟩

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