∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
  [inst_1 : DecidableEq δ] {s : Finset δ} {f : ((i : δ) → X i) → ENNReal} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)],
  Measurable f → Measurable (∫⋯∫⁻_s, f ∂μ)