Commit 2023-06-24 15:15 87438883

View on Github →

feat: port Geometry.Manifold.VectorBundle.Basic (#5444)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem chartAt_comp

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

added theorem Bundle.contMDiffAt_proj

added theorem Bundle.contMDiffAt_section

added theorem Bundle.contMDiffAt_totalSpace

added theorem Bundle.contMDiffOn_proj

added theorem Bundle.contMDiffWithinAt_proj

added theorem Bundle.contMDiffWithinAt_totalSpace

added theorem Bundle.contMDiff_proj

added theorem Bundle.smoothAt_proj

added theorem Bundle.smoothOn_proj

added theorem Bundle.smoothWithinAt_proj

added theorem Bundle.smooth_proj

added theorem Bundle.smooth_zeroSection

added theorem FiberBundle.chartedSpace'_chartAt

added theorem FiberBundle.chartedSpace_chartAt

added theorem FiberBundle.chartedSpace_chartAt_symm_fst

added theorem VectorBundleCore.smoothOn_coordChange

added theorem VectorPrebundle.mk_smoothCoordChange

added theorem VectorPrebundle.smoothCoordChange_apply

added theorem VectorPrebundle.smoothOn_smoothCoordChange

added theorem VectorPrebundle.smoothVectorBundle

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/VectorBundle/Basic.lean

added theorem VectorPrebundle.toVectorBundle

deleted theorem VectorPrebundle.to_vectorBundle