Commit 2023-06-05 05:02 9d6881f5

View on Github →

feat: port Geometry.Manifold.SmoothManifoldWithCorners (#4636)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem LocalHomeomorph.contDiffOn_extend_coord_change

added theorem LocalHomeomorph.contDiffWithinAt_extend_coord_change'

added theorem LocalHomeomorph.contDiffWithinAt_extend_coord_change

added theorem LocalHomeomorph.continuousAt_extend

added theorem LocalHomeomorph.continuousAt_extend_symm'

added theorem LocalHomeomorph.continuousAt_extend_symm

added theorem LocalHomeomorph.continuousOn_extend

added theorem LocalHomeomorph.continuousOn_extend_symm

added def LocalHomeomorph.extend

added theorem LocalHomeomorph.extend_coe

added theorem LocalHomeomorph.extend_coe_symm

added theorem LocalHomeomorph.extend_coord_change_source

added theorem LocalHomeomorph.extend_coord_change_source_mem_nhdsWithin'

added theorem LocalHomeomorph.extend_coord_change_source_mem_nhdsWithin

added theorem LocalHomeomorph.extend_image_source_inter

added theorem LocalHomeomorph.extend_left_inv

added theorem LocalHomeomorph.extend_preimage_inter_eq

added theorem LocalHomeomorph.extend_preimage_mem_nhds

added theorem LocalHomeomorph.extend_preimage_mem_nhdsWithin

added theorem LocalHomeomorph.extend_source

added theorem LocalHomeomorph.extend_source_mem_nhds

added theorem LocalHomeomorph.extend_source_mem_nhdsWithin

added theorem LocalHomeomorph.extend_symm_continuousWithinAt_comp_right_iff

added theorem LocalHomeomorph.extend_symm_preimage_inter_range_eventuallyEq

added theorem LocalHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux

added theorem LocalHomeomorph.extend_target

added theorem LocalHomeomorph.extend_target_mem_nhdsWithin

added theorem LocalHomeomorph.extend_target_subset_range

added theorem LocalHomeomorph.isOpen_extend_preimage'

added theorem LocalHomeomorph.isOpen_extend_preimage

added theorem LocalHomeomorph.isOpen_extend_source

added theorem LocalHomeomorph.map_extend_nhds

added theorem LocalHomeomorph.map_extend_nhdsWithin

added theorem LocalHomeomorph.map_extend_nhdsWithin_eq_image

added theorem LocalHomeomorph.map_extend_symm_nhdsWithin

added theorem LocalHomeomorph.map_extend_symm_nhdsWithin_range

added theorem LocalHomeomorph.mapsTo_extend

added theorem LocalHomeomorph.nhdsWithin_extend_target_eq

added theorem LocalHomeomorph.singleton_smoothManifoldWithCorners

added def ModelWithCorners.Simps.apply

added def ModelWithCorners.Simps.symm_apply

added theorem ModelWithCorners.closed_range

added theorem ModelWithCorners.continuousAt_symm

added theorem ModelWithCorners.continuousOn_symm

added theorem ModelWithCorners.continuousWithinAt_symm

added theorem ModelWithCorners.continuous_symm

added theorem ModelWithCorners.image_mem_nhdsWithin

added theorem ModelWithCorners.injective

added theorem ModelWithCorners.map_nhdsWithin_eq

added theorem ModelWithCorners.map_nhds_eq

added theorem ModelWithCorners.mk_coe

added theorem ModelWithCorners.mk_symm

added def ModelWithCorners.pi

added theorem ModelWithCorners.preimage_image

added def ModelWithCorners.prod

added theorem ModelWithCorners.range_prod

added theorem ModelWithCorners.symm_comp_self

added theorem ModelWithCorners.symm_continuousWithinAt_comp_right_iff

added theorem ModelWithCorners.symm_map_nhdsWithin_image

added theorem ModelWithCorners.symm_map_nhdsWithin_range

added def ModelWithCorners.tangent

added theorem ModelWithCorners.target_eq

added def ModelWithCorners.toFun'

added theorem ModelWithCorners.toLocalEquiv_coe

added theorem ModelWithCorners.toLocalEquiv_coe_symm

added theorem ModelWithCorners.unique_diff_at_image

added theorem ModelWithCorners.unique_diff_preimage

added theorem ModelWithCorners.unique_diff_preimage_source

added structure ModelWithCorners

added theorem OpenEmbedding.singleton_smoothManifoldWithCorners

added theorem SmoothManifoldWithCorners.chart_mem_maximalAtlas

added theorem SmoothManifoldWithCorners.compatible_of_mem_maximalAtlas

added def SmoothManifoldWithCorners.maximalAtlas

added theorem SmoothManifoldWithCorners.mk'

added theorem SmoothManifoldWithCorners.subset_maximalAtlas

added def contDiffGroupoid

added theorem contDiffGroupoid_le

added theorem contDiffGroupoid_prod

added theorem contDiffGroupoid_zero_eq

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_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_mem_nhdsWithin'

added theorem extChartAt_target_mem_nhdsWithin

added theorem extChartAt_target_subset_range

added theorem extChartAt_to_inv

added theorem ext_chart_model_space_apply

added theorem ext_coord_change_source

added theorem isOpen_extChartAt_preimage'

added theorem isOpen_extChartAt_preimage

added theorem isOpen_extChartAt_source

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_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 def modelWithCornersSelf

added theorem modelWithCornersSelf_coe

added theorem modelWithCornersSelf_coe_symm

added theorem modelWithCornersSelf_localEquiv

added theorem modelWithCornersSelf_prod

added theorem modelWithCorners_prod_coe

added theorem modelWithCorners_prod_coe_symm

added theorem modelWithCorners_prod_toLocalEquiv

added theorem nhdsWithin_extChartAt_target_eq'

added theorem nhdsWithin_extChartAt_target_eq

added theorem ofSet_mem_contDiffGroupoid

added theorem smoothManifoldWithCorners_of_contDiffOn

added theorem symm_trans_mem_contDiffGroupoid

added def writtenInExtChartAt