Theorem ContMDiffWithinAt.sum_section_of_locallyFinite

Modification history

2025-07-22 18:37
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
feat: sum of a locally finite collection of C^n sections is C^n (#27349) …
Added ContMDiffWithinAt.sum_section_of_locallyFiniteView on Github →