Commit 2024-07-22 14:24 409fa733
View on Github →feat: continuity of primitives for parametric integrals (#11185)
From the sphere eversion project and generalised by sgouezel
.
This is used in the sphere eversion project to show that averaging of loops is continuous (which will be PRed to mathlib at a later point).
Co-authored by: @fpvandoorn (who write this code originally, I believe)