Commit 2023-07-03 05:30 f32c393b

View on Github →

feat: port Geometry.Manifold.Diffeomorph (#5660)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/Diffeomorph.lean

added theorem ContinuousLinearEquiv.coe_toDiffeomorph

added theorem ContinuousLinearEquiv.coe_toDiffeomorph_symm

added theorem ContinuousLinearEquiv.symm_toDiffeomorph

added def ContinuousLinearEquiv.toDiffeomorph

added theorem Diffeomorph.apply_symm_apply

added theorem Diffeomorph.coeFn_injective

added theorem Diffeomorph.coe_coe

added theorem Diffeomorph.coe_prodComm

added theorem Diffeomorph.coe_prodCongr

added theorem Diffeomorph.coe_refl

added theorem Diffeomorph.coe_toEquiv

added theorem Diffeomorph.coe_toHomeomorph

added theorem Diffeomorph.coe_toHomeomorph_symm

added theorem Diffeomorph.coe_trans

added theorem Diffeomorph.contMDiffAt_comp_diffeomorph_iff

added theorem Diffeomorph.contMDiffAt_diffeomorph_comp_iff

added theorem Diffeomorph.contMDiffAt_transDiffeomorph_left

added theorem Diffeomorph.contMDiffAt_transDiffeomorph_right

added theorem Diffeomorph.contMDiffOn_comp_diffeomorph_iff

added theorem Diffeomorph.contMDiffOn_diffeomorph_comp_iff

added theorem Diffeomorph.contMDiffOn_transDiffeomorph_left

added theorem Diffeomorph.contMDiffOn_transDiffeomorph_right

added theorem Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff

added theorem Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff

added theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_left

added theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_right

added theorem Diffeomorph.contMDiff_comp_diffeomorph_iff

added theorem Diffeomorph.contMDiff_diffeomorph_comp_iff

added theorem Diffeomorph.contMDiff_transDiffeomorph_left

added theorem Diffeomorph.contMDiff_transDiffeomorph_right

added theorem Diffeomorph.ext

added theorem Diffeomorph.image_eq_preimage

added theorem Diffeomorph.image_symm_image

added def Diffeomorph.prodAssoc

added def Diffeomorph.prodComm

added theorem Diffeomorph.prodComm_symm

added def Diffeomorph.prodCongr

added theorem Diffeomorph.prodCongr_symm

added theorem Diffeomorph.refl_toEquiv

added theorem Diffeomorph.refl_trans

added theorem Diffeomorph.self_trans_symm

added theorem Diffeomorph.smooth_transDiffeomorph_left

added theorem Diffeomorph.smooth_transDiffeomorph_right

added theorem Diffeomorph.symm_apply_apply

added theorem Diffeomorph.symm_image_eq_preimage

added theorem Diffeomorph.symm_image_image

added theorem Diffeomorph.symm_refl

added theorem Diffeomorph.symm_toEquiv

added theorem Diffeomorph.symm_toHomeomorph

added theorem Diffeomorph.symm_trans'

added theorem Diffeomorph.symm_trans_self

added def Diffeomorph.toContMDiffMap

added theorem Diffeomorph.toEquiv_coe_symm

added theorem Diffeomorph.toEquiv_inj

added theorem Diffeomorph.toEquiv_injective

added def Diffeomorph.toHomeomorph

added theorem Diffeomorph.toHomeomorph_toEquiv

added theorem Diffeomorph.toLocalHomeomorph_mdifferentiable

added def Diffeomorph.toTransDiffeomorph

added theorem Diffeomorph.trans_refl

added theorem Diffeomorph.uniqueDiffOn_image

added theorem Diffeomorph.uniqueDiffOn_preimage

added theorem Diffeomorph.uniqueMDiffOn_image

added theorem Diffeomorph.uniqueMDiffOn_image_aux

added theorem Diffeomorph.uniqueMDiffOn_preimage

added structure Diffeomorph

added theorem ModelWithCorners.coe_extChartAt_transDiffeomorph

added theorem ModelWithCorners.coe_extChartAt_transDiffeomorph_symm

added theorem ModelWithCorners.coe_transDiffeomorph

added theorem ModelWithCorners.coe_transDiffeomorph_symm

added theorem ModelWithCorners.extChartAt_transDiffeomorph_target

added def ModelWithCorners.transDiffeomorph

added theorem ModelWithCorners.transDiffeomorph_range