Theorems · Inductive type · global analysis

Structomorph

{H : Type u} →
  [inst : TopologicalSpace H] →
    StructureGroupoid H →
      (M : Type u_5) →
        (M' : Type u_6) →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : TopologicalSpace M'] → [ChartedSpace H M] → [ChartedSpace H M'] → Type (max u_5 u_6)

A G-diffeomorphism between two charted spaces is a homeomorphism which, when read in the charts, belongs to G. We avoid the word diffeomorph as it is too related to the smooth category, and use structomorph instead.

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpace