Theorems · Definition · global analysis

Structomorph.noConfusionType

Sort u_1 →
  {H : Type u} →
    [inst : TopologicalSpace H] →
      {G : StructureGroupoid H} →
        {M : Type u_5} →
          {M' : Type u_6} →
            [inst_1 : TopologicalSpace M] →
              [inst_2 : TopologicalSpace M'] →
                [inst_3 : ChartedSpace H M] →
                  [inst_4 : ChartedSpace H M'] →
                    Structomorph G M M' →
                      {H' : Type u} →
                        [inst' : TopologicalSpace H'] →
                          {G' : StructureGroupoid H'} →
                            {M' : Type u_5} →
                              {M'' : Type u_6} →
                                [inst'_1 : TopologicalSpace M'] →
                                  [inst'_2 : TopologicalSpace M''] →
                                    [inst'_3 : ChartedSpace H' M'] →
                                      [inst'_4 : ChartedSpace H' M''] → Structomorph G' M' M'' → Sort u_1

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpace