∀ {ι : Type u_1} [Finite ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (μ : MeasureTheory.Measure (ι → ℝ))
  [MeasureTheory.IsLocallyFiniteMeasure μ], ∑ J ∈ π.boxes, μ.real ↑J = μ.real π.iUnion