Commit 2025-06-12 14:29 f3cb4ca9

View on Github →

chore: for models with corners, weaken transDiffeomomorph to transContinuousLinearEquiv (#25809) This is needed before we can switch the definition of models with corners in #23658, as general diffeomorphisms don't send convex sets to convex sets.

Estimated changes

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

added theorem ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_left

added theorem ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_right

added theorem ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_left

added theorem ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_right

added theorem ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_left

added theorem ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_right

added theorem ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_left

added theorem ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_right

added def ContinuousLinearEquiv.toTransContinuousLinearEquiv

deleted theorem Diffeomorph.contMDiffAt_transDiffeomorph_left

deleted theorem Diffeomorph.contMDiffAt_transDiffeomorph_right

deleted theorem Diffeomorph.contMDiffOn_transDiffeomorph_left

deleted theorem Diffeomorph.contMDiffOn_transDiffeomorph_right

deleted theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_left

deleted theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_right

deleted theorem Diffeomorph.contMDiff_transDiffeomorph_left

deleted theorem Diffeomorph.contMDiff_transDiffeomorph_right

deleted def Diffeomorph.toTransDiffeomorph

added theorem ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv

added theorem ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv_symm

deleted theorem ModelWithCorners.coe_extChartAt_transDiffeomorph

deleted theorem ModelWithCorners.coe_extChartAt_transDiffeomorph_symm

added theorem ModelWithCorners.coe_transContinuousLinearEquiv

added theorem ModelWithCorners.coe_transContinuousLinearEquiv_symm

deleted theorem ModelWithCorners.coe_transDiffeomorph

deleted theorem ModelWithCorners.coe_transDiffeomorph_symm

added theorem ModelWithCorners.extChartAt_transContinuousLinearEquiv_target

deleted theorem ModelWithCorners.extChartAt_transDiffeomorph_target

added def ModelWithCorners.transContinuousLinearEquiv

added theorem ModelWithCorners.transContinuousLinearEquiv_range

deleted def ModelWithCorners.transDiffeomorph

deleted theorem ModelWithCorners.transDiffeomorph_range