Theorems · Definition · global analysis

StructureGroupoid.maximalAtlas

{H : Type u} →
  (M : Type u_2) →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → StructureGroupoid H → Set (OpenPartialHomeomorph M H)

Given a charted space admitting a structure groupoid, the maximal atlas associated to this structure groupoid is the set of all charts that are compatible with the atlas, i.e., such that changing coordinates with an atlas member gives an element of the groupoid.

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

28 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceChartedSpace