Mathlib Map

Theorems · Inductive type · global analysis

HasGroupoid

{H : Type u_5} →
  [inst : TopologicalSpace H] →
    (M : Type u_6) → [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → StructureGroupoid H → Prop

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
Cited by
19 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
TopologicalSpaceTopologicalSpaceChartedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsManifold.of_le · cited by 5IsManifold.of_leStructureGroupoid.chart_mem_maximalAtlas · cited by 5StructureGroupoid.chart_m…StructureGroupoid.subset_maximalAtlas · cited by 5StructureGroupoid.subset_…StructureGroupoid.compatible · cited by 3StructureGroupoid.compati…HasGroupoid.compatible · cited by 3HasGroupoid.compatiblehasGroupoid_of_le · cited by 2hasGroupoid_of_leIsManifold.mk' · cited by 2IsManifold.mk'OpenPartialHomeomorph.singleton_hasGroupoid · cited by 1OpenPartialHomeomorph.sin…StructureGroupoid.subtypeRestr_mem_maximalAtlas · cited by 1StructureGroupoid.subtype…StructureGroupoid.trans_restricted · cited by 1StructureGroupoid.trans_r…Topology.IsOpenEmbedding.singleton_hasGroupoid · cited by 0IsOpenEmbedding.singleton…IsManifold.casesOn · cited by 0IsManifold.casesOnhasGroupoid_inf_iff · cited by 0hasGroupoid_inf_iffStructureGroupoid.HasGroupoid.comp · cited by 0HasGroupoid.comphasGroupoid_of_pregroupoid · cited by 0hasGroupoid_of_pregroupoidTopologicalSpace · cited by 24529TopologicalSpaceChartedSpace · cited by 2397ChartedSpaceStructureGroupoid · cited by 121StructureGroupoidHasGroupoidCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by25

Results whose statement or proof uses this declaration.