Commit 2023-04-11 12:17 814b0c44

View on Github →

feat: port Geometry.Manifold.ChartedSpace (#2365)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/ChartedSpace.lean

added def ChartedSpace.comp

added theorem ChartedSpace.locallyCompact

added theorem ChartedSpace.locallyConnectedSpace

added theorem ChartedSpace.secondCountable_of_countable_cover

added theorem ChartedSpace.secondCountable_of_sigma_compact

added theorem ChartedSpaceCore.open_source'

added theorem ChartedSpaceCore.open_target

added def ChartedSpaceCore.toChartedSpace

added structure ChartedSpaceCore

added def LocalHomeomorph.singletonChartedSpace

added theorem LocalHomeomorph.singletonChartedSpace_chartAt_eq

added theorem LocalHomeomorph.singletonChartedSpace_chartAt_source

added theorem LocalHomeomorph.singletonChartedSpace_mem_atlas_eq

added theorem LocalHomeomorph.singleton_hasGroupoid

added def ModelPi

added def ModelProd

added def OpenEmbedding.singletonChartedSpace

added theorem OpenEmbedding.singletonChartedSpace_chartAt_eq

added theorem OpenEmbedding.singleton_hasGroupoid

added def Pregroupoid.groupoid

added structure Pregroupoid

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.eq_on_source

added theorem StructureGroupoid.id_mem

added theorem StructureGroupoid.id_mem_maximalAtlas

added theorem StructureGroupoid.le_iff

added theorem StructureGroupoid.locality

added def StructureGroupoid.maximalAtlas

added theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid

added theorem StructureGroupoid.subset_maximalAtlas

added theorem StructureGroupoid.symm

added theorem StructureGroupoid.trans

added structure StructureGroupoid

added def achart

added theorem achart_def

added theorem achart_val

added theorem chartAt_self_eq

added theorem chart_source_mem_nhds

added theorem chart_target_mem_nhds

added theorem chartedSpaceSelf_atlas

added theorem chartedSpaceSelf_prod

added theorem closedUnderRestriction_iff_id_le

added theorem closed_under_restriction'

added theorem coe_achart

added def continuousGroupoid

added def continuousPregroupoid

added theorem groupoid_of_pregroupoid_le

added theorem hasGroupoid_of_le

added theorem hasGroupoid_of_pregroupoid

added def idGroupoid

added def idRestrGroupoid

added theorem idRestrGroupoid_mem

added theorem mem_achart_source

added theorem mem_chart_target

added theorem mem_groupoid_of_pregroupoid

added theorem mem_maximalAtlas_iff

added theorem mem_pregroupoid_of_eq_on_source

added theorem modelProd_range_prod_id

added theorem piChartedSpace_chartAt

added theorem prodChartedSpace_chartAt