case mk
M : Type u_1
ι : Type ?u.4397208
α : Type u_2
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : ι → α → M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEMeasurable f
⊢ AEMeasurable (prod (Quot.mk Setoid.r l))
M : Type u_1
ι : Type ?u.4397208
α : Type u_2
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : ι → α → M
l : Multiset (α → M)
hl : ∀ (f : α → M), f ∈ l → AEMeasurable f
⊢ AEMeasurable (prod l)
rcases l with ⟨l⟩
no goals
case mk
M : Type u_1
ι : Type ?u.4397208
α : Type u_2
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : ι → α → M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEMeasurable f
⊢ AEMeasurable (prod (Quot.mk Setoid.r l))
simpa using l.aemeasurable_prod' (by simpa using hl)
no goals
M : Type u_1
ι : Type ?u.4397208
α : Type u_2
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : ι → α → M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEMeasurable f
⊢ ∀ (f : α → M), f ∈ l → AEMeasurable f
simpa using hl