Commit 2025-03-03 11:12 dd2c9f61

feat: integrating the integral of an indicator (#22469) Prove that ∫ x, ∫ y, s.indicator (f · y) x ∂ν ∂μ = ∫ x in s, ∫ y, f x y ∂ν ∂μ, as well as a version for kernels. Create a new file for lemmas about the setIntegral against kernels to avoid large imports.