Theorems · Definition · global analysis

Structomorph.trans

{H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      {M'' : Type u_4} →
        [inst : TopologicalSpace H] →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : ChartedSpace H M] →
              [inst_3 : TopologicalSpace M'] →
                [inst_4 : TopologicalSpace M''] →
                  {G : StructureGroupoid H} →
                    [inst_5 : ChartedSpace H M'] →
                      [inst_6 : ChartedSpace H M''] → Structomorph G M M' → Structomorph G M' M'' → Structomorph G M M''

The composition of structomorphisms is a structomorphism.

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpace