Theorems · Definition · global analysis

Structomorph.recOn

{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'] →
                  {motive : Structomorph G M M' → Sort u_1} →
                    (t : Structomorph G M M') →
                      ((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) →
                            motive { toHomeomorph := toHomeomorph, mem_groupoid := mem_groupoid }) →
                        motive t

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpace