exact measurePreserving_piUnique _
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(piUnique fun i_1 => α ↑i_1).toEquiv
no goals