Commit 2023-06-26 18:00 7e6e62cb

View on Github →

feat: smoothness in a vector bundle (#5494) Add lemmas about smoothness in a smooth vector bundle. Also rename the old smoothOn_coordChange to smoothOn_coordChangeL.

Estimated changes

Modified Mathlib/Analysis/Calculus/TangentCone.lean

added theorem UniqueDiffWithinAt.congr_pt

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem mem_extChartAt_target

added theorem uniqueDiffOn_extChartAt_target

added theorem uniqueDiffWithinAt_extChartAt_target

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

modified theorem Bundle.contMDiff_proj

modified theorem Bundle.smooth_zeroSection

added theorem ContMDiffWithinAt.change_section_trivialization

added theorem Trivialization.contMDiffAt_iff

added theorem Trivialization.contMDiffOn_iff

added theorem Trivialization.contMDiffOn_symm_trans

added theorem Trivialization.contMDiffWithinAt_iff

added theorem Trivialization.contMDiffWithinAt_snd_comp_iff₂

added theorem Trivialization.contMDiff_iff

added theorem Trivialization.smoothAt_iff

added theorem Trivialization.smoothOn

added theorem Trivialization.smoothOn_iff

added theorem Trivialization.smoothOn_symm

added theorem Trivialization.smoothWithinAt_iff

added theorem Trivialization.smooth_iff

added theorem contMDiffAt_coordChangeL

added theorem contMDiffOn_coordChangeL

added theorem contMDiffOn_symm_coordChangeL

added theorem smoothAt_coordChangeL

added theorem smoothOn_coordChangeL

added theorem smoothOn_symm_coordChangeL

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