no goals
M : Type u_1
ι : Type ?u.4458135
α : Type u_2
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : ι → α → M
s : Multiset (α → M)
hs : ∀ (f : α → M), f ∈ s → Measurable f
⊢ Measurable fun x => prod (map (fun f => f x) s)
simpa only [← Pi.multiset_prod_apply] using s.measurable_prod' hs