Theorems · Theorem · global analysis

StructureGroupoid.compatible_of_mem_maximalAtlas

∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph M H},
  e ∈ StructureGroupoid.maximalAtlas M G → e' ∈ StructureGroupoid.maximalAtlas M G → e.symm.trans e' ∈ G

Changing coordinates between two elements of the maximal atlas gives rise to an element of the structure groupoid.

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceChartedSpace