mathlib

f3ae2d0d - feat(measure_theory/constructions/prod): The layercake integral. (#14424)

feat(measure_theory/constructions/prod): The layercake integral. (#14424) Prove the layercake formula, a.k.a. Cavalieri's principle, often used in measure theory and probability theory. It will in particular be a part of the proof of the portmanteau theorem. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>