Commit 2026-01-15 09:15 e484d8b1

View on Github →

refactor(Geometry/Manifold): split long file ChartedSpace.lean (#33896) Split the > 1500 line file Mathlib.Geometry.Manifold.ChartedSpace into 3 shorter files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

deleted def OpenPartialHomeomorph.singletonChartedSpace

deleted theorem OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq

deleted theorem OpenPartialHomeomorph.singletonChartedSpace_chartAt_source

deleted theorem OpenPartialHomeomorph.singletonChartedSpace_mem_atlas_eq

deleted theorem OpenPartialHomeomorph.singleton_hasGroupoid

deleted def OpenPartialHomeomorph.toStructomorph

deleted def Pregroupoid.groupoid

deleted structure Pregroupoid

deleted def Structomorph.refl

deleted def Structomorph.symm

deleted def Structomorph.trans

deleted structure Structomorph

deleted theorem StructureGroupoid.chart_mem_maximalAtlas

deleted theorem StructureGroupoid.compatible

deleted theorem StructureGroupoid.compatible_of_mem_maximalAtlas

deleted theorem StructureGroupoid.id_mem

deleted theorem StructureGroupoid.id_mem_maximalAtlas

deleted theorem StructureGroupoid.le_iff

deleted theorem StructureGroupoid.locality

deleted def StructureGroupoid.maximalAtlas

deleted theorem StructureGroupoid.maximalAtlas_mono

deleted theorem StructureGroupoid.mem_iff_of_eqOnSource

deleted theorem StructureGroupoid.mem_maximalAtlas_of_eqOnSource

deleted theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid

deleted theorem StructureGroupoid.mem_of_eqOnSource

deleted theorem StructureGroupoid.restriction_mem_maximalAtlas_subtype

deleted theorem StructureGroupoid.subset_maximalAtlas

deleted theorem StructureGroupoid.subtypeRestr_mem_maximalAtlas

deleted theorem StructureGroupoid.symm

deleted theorem StructureGroupoid.trans

deleted theorem StructureGroupoid.trans_restricted

deleted structure StructureGroupoid

deleted theorem TopologicalSpace.Opens.chartAt_eq

deleted theorem TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq

deleted theorem TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq

deleted theorem TopologicalSpace.Opens.chart_eq'

deleted theorem TopologicalSpace.Opens.chart_eq

deleted def Topology.IsOpenEmbedding.singletonChartedSpace

deleted theorem Topology.IsOpenEmbedding.singletonChartedSpace_chartAt_eq

deleted theorem Topology.IsOpenEmbedding.singleton_hasGroupoid

deleted theorem closedUnderRestriction'

deleted theorem closedUnderRestriction_iff_id_le

deleted def continuousGroupoid

deleted theorem groupoid_of_pregroupoid_le

deleted theorem hasGroupoid_inf_iff

deleted theorem hasGroupoid_of_le

deleted theorem hasGroupoid_of_pregroupoid

deleted def idGroupoid

deleted def idRestrGroupoid

deleted theorem idRestrGroupoid_mem

deleted theorem mem_groupoid_of_pregroupoid

deleted theorem mem_maximalAtlas_iff

deleted theorem mem_pregroupoid_of_eqOnSource

deleted theorem restr_mem_maximalAtlas

Modified Mathlib/Geometry/Manifold/ConformalGroupoid.lean

Created Mathlib/Geometry/Manifold/HasGroupoid.lean

added def OpenPartialHomeomorph.singletonChartedSpace

added theorem OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq

added theorem OpenPartialHomeomorph.singletonChartedSpace_chartAt_source

added theorem OpenPartialHomeomorph.singletonChartedSpace_mem_atlas_eq

added theorem OpenPartialHomeomorph.singleton_hasGroupoid

added def OpenPartialHomeomorph.toStructomorph

added def Structomorph.refl

added def Structomorph.symm

added def Structomorph.trans

added structure Structomorph

added theorem StructureGroupoid.chart_mem_maximalAtlas

added theorem StructureGroupoid.compatible

added theorem StructureGroupoid.compatible_of_mem_maximalAtlas

added theorem StructureGroupoid.id_mem_maximalAtlas

added def StructureGroupoid.maximalAtlas

added theorem StructureGroupoid.maximalAtlas_mono

added theorem StructureGroupoid.mem_maximalAtlas_of_eqOnSource

added theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid

added theorem StructureGroupoid.restriction_mem_maximalAtlas_subtype

added theorem StructureGroupoid.subset_maximalAtlas

added theorem StructureGroupoid.subtypeRestr_mem_maximalAtlas

added theorem StructureGroupoid.trans_restricted

added theorem TopologicalSpace.Opens.chartAt_eq

added theorem TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq

added theorem TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq

added theorem TopologicalSpace.Opens.chart_eq'

added theorem TopologicalSpace.Opens.chart_eq

added def Topology.IsOpenEmbedding.singletonChartedSpace

added theorem Topology.IsOpenEmbedding.singletonChartedSpace_chartAt_eq

added theorem Topology.IsOpenEmbedding.singleton_hasGroupoid

added theorem hasGroupoid_inf_iff

added theorem hasGroupoid_of_le

added theorem hasGroupoid_of_pregroupoid

added theorem mem_maximalAtlas_iff

added theorem restr_mem_maximalAtlas

Modified Mathlib/Geometry/Manifold/IsManifold/Basic.lean

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

Created Mathlib/Geometry/Manifold/StructureGroupoid.lean

added def Pregroupoid.groupoid

added structure Pregroupoid

added theorem StructureGroupoid.id_mem

added theorem StructureGroupoid.le_iff

added theorem StructureGroupoid.locality

added theorem StructureGroupoid.mem_iff_of_eqOnSource

added theorem StructureGroupoid.mem_of_eqOnSource

added theorem StructureGroupoid.symm

added theorem StructureGroupoid.trans

added structure StructureGroupoid

added theorem closedUnderRestriction'

added theorem closedUnderRestriction_iff_id_le

added def continuousGroupoid

added theorem groupoid_of_pregroupoid_le

added def idGroupoid

added def idRestrGroupoid

added theorem idRestrGroupoid_mem

added theorem mem_groupoid_of_pregroupoid

added theorem mem_pregroupoid_of_eqOnSource