case mk
α : Type u_1
β : Type ?u.116204
γ : Type ?u.116207
ι : Type ?u.116210
inst✝³ : Countable ι
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → StronglyMeasurable f
⊢ StronglyMeasurable (Multiset.prod (Quot.mk Setoid.r l))
α : Type u_1
β : Type ?u.116204
γ : Type ?u.116207
ι : Type ?u.116210
inst✝³ : Countable ι
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l : Multiset (α → M)
hl : ∀ (f : α → M), f ∈ l → StronglyMeasurable f
⊢ StronglyMeasurable (Multiset.prod l)
rcases l with ⟨l⟩
no goals
case mk
α : Type u_1
β : Type ?u.116204
γ : Type ?u.116207
ι : Type ?u.116210
inst✝³ : Countable ι
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → StronglyMeasurable f
⊢ StronglyMeasurable (Multiset.prod (Quot.mk Setoid.r l))
simpa using l.stronglyMeasurable_prod' (by simpa using hl)
no goals
α : Type u_1
β : Type ?u.116204
γ : Type ?u.116207
ι : Type ?u.116210
inst✝³ : Countable ι
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → StronglyMeasurable f
⊢ ∀ (f : α → M), f ∈ l → StronglyMeasurable f
simpa using hl