Commit 2024-12-09 17:46 3c0727b0

View on Github →

feat: the homeomorphism between the tangent bundle to the model space and the product is a diffeomorphism (#19637)

Estimated changes

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

added def tangentBundleModelSpaceDiffeomorph

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

added theorem UniqueMDiffOn.uniqueDiffWithinAt_range_inter

added theorem UniqueMDiffOn.uniqueMDiffOn_target_inter

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

added theorem contMDiffAt_vectorSpace_iff_contDiffAt

added theorem contMDiffOn_vectorSpace_iff_contDiffOn

added theorem contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt

added theorem contMDiff_snd_tangentBundle_modelSpace

added theorem contMDiff_tangentBundleModelSpaceHomeomorph

added theorem contMDiff_tangentBundleModelSpaceHomeomorph_symm

added theorem contMDiff_vectorSpace_iff_contDiff

added theorem trivializationAt_model_space_apply