α✝ : Type ?u.4535638
α' : Type ?u.4535641
β✝ : Type ?u.4535644
β' : Type ?u.4535647
γ✝ : Type ?u.4535650
E : Type ?u.4535653
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : MeasurableSpace α'
inst✝⁸ : MeasurableSpace β✝
inst✝⁷ : MeasurableSpace β'
inst✝⁶ : MeasurableSpace γ✝
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ✝ : Measure γ✝
inst✝⁵ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving fun x => f (x, y)
⊢ QuasiMeasurePreserving f
α✝ : Type ?u.4535638
α' : Type ?u.4535641
β✝ : Type ?u.4535644
β' : Type ?u.4535647
γ✝ : Type ?u.4535650
E : Type ?u.4535653
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : MeasurableSpace α'
inst✝⁸ : MeasurableSpace β✝
inst✝⁷ : MeasurableSpace β'
inst✝⁶ : MeasurableSpace γ✝
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ✝ : Measure γ✝
inst✝⁵ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving fun x => f (x, y)
⊢ QuasiMeasurePreserving f
rw [← prod_swap]
no goals
α✝ : Type ?u.4535638
α' : Type ?u.4535641
β✝ : Type ?u.4535644
β' : Type ?u.4535647
γ✝ : Type ?u.4535650
E : Type ?u.4535653
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : MeasurableSpace α'
inst✝⁸ : MeasurableSpace β✝
inst✝⁷ : MeasurableSpace β'
inst✝⁶ : MeasurableSpace γ✝
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ✝ : Measure γ✝
inst✝⁵ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving fun x => f (x, y)
⊢ QuasiMeasurePreserving f
convert (QuasiMeasurePreserving.prod_of_right (hf.comp measurable_swap) h2f).comp
    ((measurable_swap.measurePreserving (ν.prod μ)).symm
        MeasurableEquiv.prodComm).quasiMeasurePreserving