Theorems · Theorem · global analysis

StructureGroupoid.compatible_of_mem_maximalAtlas_left

∀ {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} {x : M},
  e' ∈ StructureGroupoid.maximalAtlas M G → e'.symm.trans (chartAt H x) ∈ G

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceChartedSpace