Commit 2025-02-04 15:13 b4c61c01

View on Github →

chore(Geometry/Manifold/IsManifold): split out material on extended charts (#21219) Fixes a longFile linter warning. A few lemmas about topological manifolds also used extended charts, hence were moved to the new file also.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

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

deleted theorem ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq

deleted theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range

deleted theorem FiniteDimensional.of_locallyCompact_manifold

deleted theorem LocallyCompactSpace.of_locallyCompact_manifold

deleted theorem Manifold.locallyCompact_of_finiteDimensional

deleted theorem PartialHomeomorph.contDiffOn_extend_coord_change

deleted theorem PartialHomeomorph.contDiffWithinAt_extend_coord_change'

deleted theorem PartialHomeomorph.contDiffWithinAt_extend_coord_change

deleted theorem PartialHomeomorph.continuousAt_extend

deleted theorem PartialHomeomorph.continuousAt_extend_symm'

deleted theorem PartialHomeomorph.continuousAt_extend_symm

deleted theorem PartialHomeomorph.continuousOn_extend

deleted theorem PartialHomeomorph.continuousOn_extend_symm

deleted theorem PartialHomeomorph.continuousOn_writtenInExtend_iff

deleted theorem PartialHomeomorph.continuousWithinAt_writtenInExtend_iff

deleted def PartialHomeomorph.extend

deleted theorem PartialHomeomorph.extend_coe

deleted theorem PartialHomeomorph.extend_coe_symm

deleted theorem PartialHomeomorph.extend_coord_change_source

deleted theorem PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin'

deleted theorem PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin

deleted theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_boundaryless

deleted theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_mem_interior_range

deleted theorem PartialHomeomorph.extend_image_source_inter

deleted theorem PartialHomeomorph.extend_left_inv'

deleted theorem PartialHomeomorph.extend_left_inv

deleted theorem PartialHomeomorph.extend_preimage_inter_eq

deleted theorem PartialHomeomorph.extend_preimage_mem_nhds

deleted theorem PartialHomeomorph.extend_preimage_mem_nhdsWithin

deleted theorem PartialHomeomorph.extend_source

deleted theorem PartialHomeomorph.extend_source_mem_nhds

deleted theorem PartialHomeomorph.extend_source_mem_nhdsWithin

deleted theorem PartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff

deleted theorem PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq

deleted theorem PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux

deleted theorem PartialHomeomorph.extend_target'

deleted theorem PartialHomeomorph.extend_target

deleted theorem PartialHomeomorph.extend_target_eventuallyEq

deleted theorem PartialHomeomorph.extend_target_mem_nhdsWithin

deleted theorem PartialHomeomorph.extend_target_subset_range

deleted theorem PartialHomeomorph.interior_extend_target_subset_interior_range

deleted theorem PartialHomeomorph.isOpen_extend_preimage'

deleted theorem PartialHomeomorph.isOpen_extend_preimage

deleted theorem PartialHomeomorph.isOpen_extend_source

deleted theorem PartialHomeomorph.isOpen_extend_target

deleted theorem PartialHomeomorph.map_extend_nhds

deleted theorem PartialHomeomorph.map_extend_nhdsWithin

deleted theorem PartialHomeomorph.map_extend_nhdsWithin_eq_image

deleted theorem PartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset

deleted theorem PartialHomeomorph.map_extend_nhds_of_boundaryless

deleted theorem PartialHomeomorph.map_extend_nhds_of_mem_interior_range

deleted theorem PartialHomeomorph.map_extend_symm_nhdsWithin

deleted theorem PartialHomeomorph.map_extend_symm_nhdsWithin_range

deleted theorem PartialHomeomorph.mapsTo_extend

deleted theorem PartialHomeomorph.mem_interior_extend_target

deleted theorem PartialHomeomorph.nhdsWithin_extend_target_eq

deleted theorem PartialHomeomorph.tendsto_extend_comp_iff

deleted theorem contDiffOn_ext_coord_change

deleted theorem contDiffWithinAt_ext_coord_change

deleted theorem continuousAt_extChartAt'

deleted theorem continuousAt_extChartAt

deleted theorem continuousAt_extChartAt_symm''

deleted theorem continuousAt_extChartAt_symm'

deleted theorem continuousAt_extChartAt_symm

deleted theorem continuousOn_extChartAt

deleted theorem continuousOn_extChartAt_symm

deleted def extChartAt

deleted theorem extChartAt_coe

deleted theorem extChartAt_coe_symm

deleted theorem extChartAt_comp

deleted theorem extChartAt_image_nhd_mem_nhds_of_boundaryless

deleted theorem extChartAt_image_nhd_mem_nhds_of_mem_interior_range

deleted theorem extChartAt_mem_closure_interior

deleted theorem extChartAt_model_space_eq_id

deleted theorem extChartAt_preimage_inter_eq

deleted theorem extChartAt_preimage_mem_nhds'

deleted theorem extChartAt_preimage_mem_nhds

deleted theorem extChartAt_preimage_mem_nhdsWithin'

deleted theorem extChartAt_preimage_mem_nhdsWithin

deleted theorem extChartAt_prod

deleted theorem extChartAt_self_apply

deleted theorem extChartAt_self_eq

deleted theorem extChartAt_source

deleted theorem extChartAt_source_mem_nhds'

deleted theorem extChartAt_source_mem_nhds

deleted theorem extChartAt_source_mem_nhdsWithin'

deleted theorem extChartAt_source_mem_nhdsWithin

deleted theorem extChartAt_target

deleted theorem extChartAt_target_eventuallyEq'

deleted theorem extChartAt_target_eventuallyEq

deleted theorem extChartAt_target_eventuallyEq_of_mem

deleted theorem extChartAt_target_mem_nhds'

deleted theorem extChartAt_target_mem_nhds

deleted theorem extChartAt_target_mem_nhdsWithin'

deleted theorem extChartAt_target_mem_nhdsWithin

deleted theorem extChartAt_target_mem_nhdsWithin_of_mem

deleted theorem extChartAt_target_subset_closure_interior

deleted theorem extChartAt_target_subset_range

deleted theorem extChartAt_target_union_compl_range_mem_nhds_of_mem

deleted theorem extChartAt_to_inv

deleted theorem ext_chart_model_space_apply

deleted theorem ext_coord_change_source

deleted theorem interior_extChartAt_target_nonempty

deleted theorem isOpen_extChartAt_preimage'

deleted theorem isOpen_extChartAt_preimage

deleted theorem isOpen_extChartAt_source

deleted theorem isOpen_extChartAt_target

deleted theorem map_extChartAt_nhds'

deleted theorem map_extChartAt_nhds

deleted theorem map_extChartAt_nhdsWithin'

deleted theorem map_extChartAt_nhdsWithin

deleted theorem map_extChartAt_nhdsWithin_eq_image'

deleted theorem map_extChartAt_nhdsWithin_eq_image

deleted theorem map_extChartAt_nhds_of_boundaryless

deleted theorem map_extChartAt_symm_nhdsWithin'

deleted theorem map_extChartAt_symm_nhdsWithin

deleted theorem map_extChartAt_symm_nhdsWithin_range'

deleted theorem map_extChartAt_symm_nhdsWithin_range

deleted theorem mapsTo_extChartAt

deleted theorem mem_extChartAt_source

deleted theorem mem_extChartAt_target

deleted theorem nhdsWithin_extChartAt_target_eq'

deleted theorem nhdsWithin_extChartAt_target_eq

deleted theorem nhdsWithin_extChartAt_target_eq_of_mem

deleted theorem uniqueDiffOn_extChartAt_target

deleted theorem uniqueDiffWithinAt_extChartAt_target

deleted def writtenInExtChartAt

deleted theorem writtenInExtChartAt_chartAt

deleted theorem writtenInExtChartAt_chartAt_comp

deleted theorem writtenInExtChartAt_chartAt_symm

deleted theorem writtenInExtChartAt_chartAt_symm_comp

deleted theorem writtenInExtChartAt_extChartAt

deleted theorem writtenInExtChartAt_extChartAt_symm

Created Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

added theorem ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq

added theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range

added theorem FiniteDimensional.of_locallyCompact_manifold

added theorem LocallyCompactSpace.of_locallyCompact_manifold

added theorem Manifold.locallyCompact_of_finiteDimensional

added theorem PartialHomeomorph.contDiffOn_extend_coord_change

added theorem PartialHomeomorph.contDiffWithinAt_extend_coord_change'

added theorem PartialHomeomorph.contDiffWithinAt_extend_coord_change

added theorem PartialHomeomorph.continuousAt_extend

added theorem PartialHomeomorph.continuousAt_extend_symm'

added theorem PartialHomeomorph.continuousAt_extend_symm

added theorem PartialHomeomorph.continuousOn_extend

added theorem PartialHomeomorph.continuousOn_extend_symm

added theorem PartialHomeomorph.continuousOn_writtenInExtend_iff

added theorem PartialHomeomorph.continuousWithinAt_writtenInExtend_iff

added def PartialHomeomorph.extend

added theorem PartialHomeomorph.extend_coe

added theorem PartialHomeomorph.extend_coe_symm

added theorem PartialHomeomorph.extend_coord_change_source

added theorem PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin'

added theorem PartialHomeomorph.extend_coord_change_source_mem_nhdsWithin

added theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_boundaryless

added theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_mem_interior_range

added theorem PartialHomeomorph.extend_image_source_inter

added theorem PartialHomeomorph.extend_left_inv'

added theorem PartialHomeomorph.extend_left_inv

added theorem PartialHomeomorph.extend_preimage_inter_eq

added theorem PartialHomeomorph.extend_preimage_mem_nhds

added theorem PartialHomeomorph.extend_preimage_mem_nhdsWithin

added theorem PartialHomeomorph.extend_source

added theorem PartialHomeomorph.extend_source_mem_nhds

added theorem PartialHomeomorph.extend_source_mem_nhdsWithin

added theorem PartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff

added theorem PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq

added theorem PartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux

added theorem PartialHomeomorph.extend_target'

added theorem PartialHomeomorph.extend_target

added theorem PartialHomeomorph.extend_target_eventuallyEq

added theorem PartialHomeomorph.extend_target_mem_nhdsWithin

added theorem PartialHomeomorph.extend_target_subset_range

added theorem PartialHomeomorph.interior_extend_target_subset_interior_range

added theorem PartialHomeomorph.isOpen_extend_preimage'

added theorem PartialHomeomorph.isOpen_extend_preimage

added theorem PartialHomeomorph.isOpen_extend_source

added theorem PartialHomeomorph.isOpen_extend_target

added theorem PartialHomeomorph.map_extend_nhds

added theorem PartialHomeomorph.map_extend_nhdsWithin

added theorem PartialHomeomorph.map_extend_nhdsWithin_eq_image

added theorem PartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset

added theorem PartialHomeomorph.map_extend_nhds_of_boundaryless

added theorem PartialHomeomorph.map_extend_nhds_of_mem_interior_range

added theorem PartialHomeomorph.map_extend_symm_nhdsWithin

added theorem PartialHomeomorph.map_extend_symm_nhdsWithin_range

added theorem PartialHomeomorph.mapsTo_extend

added theorem PartialHomeomorph.mem_interior_extend_target

added theorem PartialHomeomorph.nhdsWithin_extend_target_eq

added theorem PartialHomeomorph.tendsto_extend_comp_iff

added theorem contDiffOn_ext_coord_change

added theorem contDiffWithinAt_ext_coord_change

added theorem continuousAt_extChartAt'

added theorem continuousAt_extChartAt

added theorem continuousAt_extChartAt_symm''

added theorem continuousAt_extChartAt_symm'

added theorem continuousAt_extChartAt_symm

added theorem continuousOn_extChartAt

added theorem continuousOn_extChartAt_symm

added def extChartAt

added theorem extChartAt_coe

added theorem extChartAt_coe_symm

added theorem extChartAt_comp

added theorem extChartAt_image_nhd_mem_nhds_of_boundaryless

added theorem extChartAt_image_nhd_mem_nhds_of_mem_interior_range

added theorem extChartAt_mem_closure_interior

added theorem extChartAt_model_space_eq_id

added theorem extChartAt_preimage_inter_eq

added theorem extChartAt_preimage_mem_nhds'

added theorem extChartAt_preimage_mem_nhds

added theorem extChartAt_preimage_mem_nhdsWithin'

added theorem extChartAt_preimage_mem_nhdsWithin

added theorem extChartAt_prod

added theorem extChartAt_self_apply

added theorem extChartAt_self_eq

added theorem extChartAt_source

added theorem extChartAt_source_mem_nhds'

added theorem extChartAt_source_mem_nhds

added theorem extChartAt_source_mem_nhdsWithin'

added theorem extChartAt_source_mem_nhdsWithin

added theorem extChartAt_target

added theorem extChartAt_target_eventuallyEq'

added theorem extChartAt_target_eventuallyEq

added theorem extChartAt_target_eventuallyEq_of_mem

added theorem extChartAt_target_mem_nhds'

added theorem extChartAt_target_mem_nhds

added theorem extChartAt_target_mem_nhdsWithin'

added theorem extChartAt_target_mem_nhdsWithin

added theorem extChartAt_target_mem_nhdsWithin_of_mem

added theorem extChartAt_target_subset_closure_interior

added theorem extChartAt_target_subset_range

added theorem extChartAt_target_union_compl_range_mem_nhds_of_mem

added theorem extChartAt_to_inv

added theorem ext_chart_model_space_apply

added theorem ext_coord_change_source

added theorem interior_extChartAt_target_nonempty

added theorem isOpen_extChartAt_preimage'

added theorem isOpen_extChartAt_preimage

added theorem isOpen_extChartAt_source

added theorem isOpen_extChartAt_target

added theorem map_extChartAt_nhds'

added theorem map_extChartAt_nhds

added theorem map_extChartAt_nhdsWithin'

added theorem map_extChartAt_nhdsWithin

added theorem map_extChartAt_nhdsWithin_eq_image'

added theorem map_extChartAt_nhdsWithin_eq_image

added theorem map_extChartAt_nhds_of_boundaryless

added theorem map_extChartAt_symm_nhdsWithin'

added theorem map_extChartAt_symm_nhdsWithin

added theorem map_extChartAt_symm_nhdsWithin_range'

added theorem map_extChartAt_symm_nhdsWithin_range

added theorem mapsTo_extChartAt

added theorem mem_extChartAt_source

added theorem mem_extChartAt_target

added theorem nhdsWithin_extChartAt_target_eq'

added theorem nhdsWithin_extChartAt_target_eq

added theorem nhdsWithin_extChartAt_target_eq_of_mem

added theorem uniqueDiffOn_extChartAt_target

added theorem uniqueDiffWithinAt_extChartAt_target

added def writtenInExtChartAt

added theorem writtenInExtChartAt_chartAt

added theorem writtenInExtChartAt_chartAt_comp

added theorem writtenInExtChartAt_chartAt_symm

added theorem writtenInExtChartAt_chartAt_symm_comp

added theorem writtenInExtChartAt_extChartAt

added theorem writtenInExtChartAt_extChartAt_symm

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

Modified Mathlib/Geometry/Manifold/MFDeriv/Defs.lean