Theorems · Definition · global analysis

Structomorph.mk.noConfusion

{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'} →
                  {P : Sort u_1} →
                    {toHomeomorph : M ≃ₜ M'} →
                      {mem_groupoid :
                          ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
                            c ∈ atlas H M →
                              c' ∈ atlas H M' → c.symm.trans (toHomeomorph.toOpenPartialHomeomorph.trans c') ∈ G} →
                        {toHomeomorph' : M ≃ₜ M'} →
                          {mem_groupoid' :
                              ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
                                c ∈ atlas H M →
                                  c' ∈ atlas H M' → c.symm.trans (toHomeomorph'.toOpenPartialHomeomorph.trans c') ∈ G} →
                            { toHomeomorph := toHomeomorph, mem_groupoid := mem_groupoid } =
                                { toHomeomorph := toHomeomorph', mem_groupoid := mem_groupoid' } →
                              (toHomeomorph ≍ toHomeomorph' → P) → P

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

1 results in Mathlib

Foundations

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