Structures · Geometry
HasGroupoid
A charted space has an atlas in a groupoid G if the change of coordinates belong to the
groupoid.
- Defined in
- Mathlib.Geometry.Manifold.HasGroupoid
- Shape
- 2 explicit arguments · adds compatible
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- StructureGroupoid.subset_maximalAtlas
- StructureGroupoid.chart_mem_maximalAtlas
- HasGroupoid.compatible
- StructureGroupoid.compatible
- IsManifold.mk'
- StructureGroupoid.trans_restricted
- StructureGroupoid.subtypeRestr_mem_maximalAtlas
- StructureGroupoid.HasGroupoid.comp
- StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm
- StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm
- StructureGroupoid.LocalInvariantProp.liftPropOn_chart
- Structomorph.refl
- OpenPartialHomeomorph.toStructomorph
- TopCat.of.hasGroupoid
- TopologicalSpace.Opens.instHasGroupoid
- StructureGroupoid.LocalInvariantProp.liftPropAt_chart
- StructureGroupoid.restriction_mem_maximalAtlas_subtype
Ancestors0
No ancestors.