no goals
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
π₁ : TaggedPrepartition I
π₂ : Prepartition I
hU : Prepartition.iUnion π₂ = ↑I \ iUnion π₁
r : (ι → ℝ) → ↑(Ioi 0)
⊢ distortion (unionComplToSubordinate π₁ π₂ hU r) = max (distortion π₁) (Prepartition.distortion π₂)
simp [unionComplToSubordinate]