Commit 2025-07-22 18:37 3bfbd0e5

View on Github →

feat: sum of a locally finite collection of C^n sections is C^n (#27349) This can be used to golf #26875 (and is nice API anyway). As such, it is necessary to prove the existence of a Riemannian metric (hence of a Levi-Civita connection). One could say it's on the path towards the Levi-Civita connection.

Estimated changes

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

modified theorem ContMDiff.sum_section

added theorem ContMDiff.sum_section_of_locallyFinite

modified theorem ContMDiffAt.sum_section

added theorem ContMDiffAt.sum_section_of_locallyFinite

modified theorem ContMDiffOn.smul_section_of_tsupport

modified theorem ContMDiffOn.sum_section

added theorem ContMDiffOn.sum_section_of_locallyFinite

modified theorem ContMDiffWithinAt.sum_section

added theorem ContMDiffWithinAt.sum_section_of_locallyFinite