Theorems · Inductive type · global analysis

StructureGroupoid

(H : Type u_2) → [TopologicalSpace H] → Type u_2

A structure groupoid is a set of open partial homeomorphisms of a topological space stable under composition and inverse. They appear in the definition of the smoothness class of a manifold.

Defined in

Mathlib.Geometry.Manifold.StructureGroupoid

Cited by

121 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpace