Commit 2026-06-11 13:02 ae9f73ad

View on Github →

feat: drop HasGroupoid assumption in several LiftPropAt lemmas (#40475)

Estimated changes

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

modified theorem contMDiffAt_extChartAt'

modified theorem contMDiffOn_chart

modified theorem contMDiffOn_chart_symm

modified theorem contMDiffOn_extChartAt

modified theorem contMDiffOn_extChartAt_symm

modified theorem contMDiffWithinAt_extChartAt_symm_range

modified theorem contMDiffWithinAt_extChartAt_symm_target

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

modified theorem contMDiffAt_iff_of_mem_source

modified theorem contMDiffOn_iff

modified theorem contMDiffOn_iff_of_subset_source'

modified theorem contMDiffOn_iff_of_subset_source

modified theorem contMDiffOn_iff_target

modified theorem contMDiffWithinAt_iff_of_mem_source'

modified theorem contMDiffWithinAt_iff_of_mem_source

modified theorem contMDiff_iff

modified theorem contMDiff_iff_target

Modified Mathlib/Geometry/Manifold/HasGroupoid.lean

added theorem StructureGroupoid.compatible_of_mem_maximalAtlas_left

added theorem StructureGroupoid.compatible_of_mem_maximalAtlas_right

Modified Mathlib/Geometry/Manifold/Immersion.lean

modified theorem Manifold.IsImmersion.contMDiff

modified theorem Manifold.IsImmersionOfComplement.contMDiff

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

added theorem StructureGroupoid.LocalInvariantProp.congr_set_fun

modified theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas

modified theorem StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas

modified theorem StructureGroupoid.LocalInvariantProp.liftPropOn_indep_chart

modified theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas

modified theorem StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas

modified theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart'

modified theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux'

modified theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source

modified theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source_aux

modified theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target

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

modified theorem mdifferentiableAt_iff_of_mem_source

modified theorem mdifferentiableOn_iff_of_subset_source'

modified theorem mdifferentiableOn_iff_of_subset_source

modified theorem mdifferentiableWithinAt_iff_of_mem_source'

modified theorem mdifferentiableWithinAt_iff_of_mem_source

Modified Mathlib/Geometry/Manifold/SmoothEmbedding.lean

modified theorem Manifold.IsSmoothEmbedding.contMDiff