Theorems · Definition · global analysis

Structomorph.noConfusion

{P : 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'} →
                    {t : Structomorph G M M'} →
                      {H' : Type u} →
                        {inst' : TopologicalSpace H'} →
                          {G' : StructureGroupoid H'} →
                            {M'_1 : Type u_5} →
                              {M'' : Type u_6} →
                                {inst'_1 : TopologicalSpace M'_1} →
                                  {inst'_2 : TopologicalSpace M''} →
                                    {inst'_3 : ChartedSpace H' M'_1} →
                                      {inst'_4 : ChartedSpace H' M''} →
                                        {t' : Structomorph G' M'_1 M''} →
                                          H = H' →
                                            inst ≍ inst' →
                                              G ≍ G' →
                                                M = M'_1 →
                                                  M' = M'' →
                                                    inst_1 ≍ inst'_1 →
                                                      inst_2 ≍ inst'_2 →
                                                        inst_3 ≍ inst'_3 →
                                                          inst_4 ≍ inst'_4 →
                                                            t ≍ t' → Structomorph.noConfusionType P t t'

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

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