α : Type u_1
β : Type ?u.8515
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (μ : Measure α), ↑↑μ s ∂b
α : Type u_1
β : Type ?u.8515
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(join b) s
simp only [join_apply hs]
no goals
α : Type u_1
β : Type ?u.8515
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (μ : Measure α), ↑↑μ s ∂b
exact measurable_lintegral (measurable_coe hs)