α : Type u_2
α' : Type ?u.4452406
β : Type u_1
β' : Type ?u.4452412
γ : Type ?u.4452415
E : Type ?u.4452418
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
h2s : ↑↑ν s = 0
⊢ ↑↑(map Prod.snd (Measure.prod μ ν)) s = 0
α : Type u_2
α' : Type ?u.4452406
β : Type u_1
β' : Type ?u.4452412
γ : Type ?u.4452415
E : Type ?u.4452418
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
⊢ QuasiMeasurePreserving Prod.snd
refine' ⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => _⟩
no goals
α : Type u_2
α' : Type ?u.4452406
β : Type u_1
β' : Type ?u.4452412
γ : Type ?u.4452415
E : Type ?u.4452418
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
h2s : ↑↑ν s = 0
⊢ ↑↑(map Prod.snd (Measure.prod μ ν)) s = 0
rw [map_apply measurable_snd hs, ← univ_prod, prod_prod, h2s, MulZeroClass.mul_zero]