Commit 2025-07-07 20:08 bacc86cc

View on Github →

feat(VectorBundle/MDifferentiable): add some basic API (#26865) mirroring the development in VectorBundle/Basic. From the path towards geodesics and the Levi-Civita connection.

Estimated changes

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

added theorem Bundle.mdifferentiableAt_proj

added theorem Bundle.mdifferentiableAt_zeroSection

added theorem Bundle.mdifferentiableOn_proj

added theorem Bundle.mdifferentiableOn_zeroSection

added theorem Bundle.mdifferentiableWithinAt_proj

added theorem Bundle.mdifferentiableWithinAt_zeroSection

added theorem Bundle.mdifferentiable_proj

added theorem Bundle.mdifferentiable_zeroSection

added theorem mdifferentiableAt_section

added theorem mdifferentiableWithinAt_section