Theorems · Theorem · global analysis

HasGroupoid.compatible

∀ {H : Type u_5} {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} {inst_2 : ChartedSpace H M}
  {G : StructureGroupoid H} [self : HasGroupoid M G] {e e' : OpenPartialHomeomorph M H},
  e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

3 results in Mathlib

Foundations

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

Assumes

HasGroupoid