Theorems · Theorem · global analysis

OpenPartialHomeomorph.singleton_hasGroupoid

∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] (e : OpenPartialHomeomorph α H)
  (h : e.source = Set.univ) (G : StructureGroupoid H) [ClosedUnderRestriction G], HasGroupoid α G

Given an open partial homeomorphism e from a space α into H, if its source covers the whole space α, then the induced charted space structure on α is HasGroupoid G for any structure groupoid G which is closed under restrictions.

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceClosedUnderRestriction