Theorems · Theorem · global analysis

StructureGroupoid.subtypeRestr_mem_maximalAtlas

∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {e : OpenPartialHomeomorph M H},
  e ∈ atlas H M →
    ∀ {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) {G : StructureGroupoid H} [HasGroupoid M G]
      [ClosedUnderRestriction G], e.subtypeRestr hs ∈ StructureGroupoid.maximalAtlas (↥s) G

Restricting a chart of M to an open subset s yields a chart in the maximal atlas of s. NB. We cannot deduce membership in atlas H s in general: by definition, this atlas contains precisely the restriction of each preferred chart at x ∈ s whereas atlas H M can contain more charts than these.

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceHasGroupoidClosedUnderRestriction