case mk
α : Type u_1
β : Type ?u.316502
γ : Type ?u.316505
ι : Type ?u.316508
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (Multiset.prod (Quot.mk Setoid.r l)) μ
α : Type u_1
β : Type ?u.316502
γ : Type ?u.316505
ι : Type ?u.316508
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : Multiset (α → M)
hl : ∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (Multiset.prod l) μ
rcases l with ⟨l⟩
no goals
case mk
α : Type u_1
β : Type ?u.316502
γ : Type ?u.316505
ι : Type ?u.316508
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (Multiset.prod (Quot.mk Setoid.r l)) μ
simpa using l.aestronglyMeasurable_prod' (by simpa using hl)
no goals
α : Type u_1
β : Type ?u.316502
γ : Type ?u.316505
ι : Type ?u.316508
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEStronglyMeasurable f μ
⊢ ∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ
simpa using hl