no goals
α : Type u_1
β : Type ?u.113287
γ : Type ?u.113290
ι : Type ?u.113293
inst✝³ : Countable ι
f g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → StronglyMeasurable f
⊢ StronglyMeasurable fun x => List.prod (List.map (fun f => f x) l)
simpa only [← Pi.list_prod_apply] using l.stronglyMeasurable_prod' hl