Theorems · Definition · global analysis

Structomorph.toHomeomorph

{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' → M ≃ₜ M'

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

1 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpace