Commit 2024-03-04 13:19 b4d17851

feat: primitive of a parametrised integral is continuous (#11110) if it is bounded by an integrable function: by the dominated convergence theorem. From the sphere-eversion project. The first two commits are preliminary clean-up; happy to split these into a separate PR.