theorem
MeasureTheory.AEMeasurable.lintegral_prod_right'
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
[SFinite ν]
⦃f : α × β → ENNReal⦄
(hf : AEMeasurable f (μ.prod ν))
:
theorem
MeasureTheory.AEMeasurable.lintegral_prod_right
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
[SFinite ν]
{f : α → β → ENNReal}
(hf : AEMeasurable (Function.uncurry f) (μ.prod ν))
:
AEMeasurable (fun (x : α) => ∫⁻ (y : β), f x y ∂ν) μ