Commit 2025-09-15 19:33 9ccb6e7c

View on Github →

feat: mdifferentiableOn_section_of_mem_baseSet₀ (#26870) The MDifferentiable analogue of contMDiffOn_section_of_mem_baseSet₀. From the path towards geodesics and the Levi-Civita connection.

Estimated changes

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

added theorem Trivialization.contMDiffAt_section_iff

added theorem Trivialization.contMDiffOn_section_baseSet_iff

added theorem Trivialization.contMDiffOn_section_iff

deleted theorem contMDiffAt_section_of_mem_baseSet

deleted theorem contMDiffOn_section_of_mem_baseSet

deleted theorem contMDiffOn_section_of_mem_baseSet₀

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

added theorem MDifferentiableWithinAt.change_section_trivialization

added theorem Trivialization.mdifferentiableAt_section_iff

added theorem Trivialization.mdifferentiableAt_snd_comp_iff₂

added theorem Trivialization.mdifferentiableAt_totalSpace_iff

added theorem Trivialization.mdifferentiableOn_section_baseSet_iff

added theorem Trivialization.mdifferentiableOn_section_iff

added theorem Trivialization.mdifferentiableWithinAt_section_iff

added theorem Trivialization.mdifferentiableWithinAt_snd_comp_iff₂

added theorem Trivialization.mdifferentiableWithinAt_totalSpace_iff