∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι] (hJ : J ≤ I)
  (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsSubordinate r =
    (BoxIntegral.Box.Icc J ⊆ Metric.closedBall x ↑(r x))