case h.e'_1.a
α : Type u_1
α' : Type ?u.2403525
β : Type u_2
β' : Type ?u.2403531
γ : Type ?u.2403534
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ Integrable f ↔ Integrable fun z => f (Prod.swap z)
α : Type u_1
α' : Type ?u.2403525
β : Type u_2
β' : Type ?u.2403531
γ : Type ?u.2403534
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ Integrable f ↔ (∀ᵐ (y : β) ∂ν, Integrable fun x => f (x, y)) ∧ Integrable fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ
convert integrable_prod_iff h1f.prod_swap using 1
no goals
case h.e'_1.a
α : Type u_1
α' : Type ?u.2403525
β : Type u_2
β' : Type ?u.2403531
γ : Type ?u.2403534
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ Integrable f ↔ Integrable fun z => f (Prod.swap z)
rw [funext fun _ => Function.comp_apply.symm, integrable_swap_iff]