[Merged by Bors] - feat: sections of a fiber bundle with Subsingleton fiber are smooth and differentiable#41027

grunweg wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:cndiff-section-subsingletongrunweg/mathlib4:cndiff-section-subsingletonCopy head branch name to clipboard