Theorems · Theorem · global analysis

Structomorph.mk.inj

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

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

1 results in Mathlib

Foundations

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