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