Theorems · Definition · global analysis

OpenPartialHomeomorph.toStructomorph

{H : Type u} →
  {M : Type u_2} →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : ChartedSpace H M] →
          {G : StructureGroupoid H} →
            {e : OpenPartialHomeomorph M H} →
              e ∈ atlas H M →
                [HasGroupoid M G] →
                  [ClosedUnderRestriction G] →
                    have s := { carrier := e.source, is_open' := ⋯ };
                    have t := { carrier := e.target, is_open' := ⋯ };
                    Structomorph G ↥s ↥t

Each chart of a charted space is a structomorphism between its source and target.

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceHasGroupoidClosedUnderRestriction