α : Type u_2
α' : Type ?u.1147235
β : Type u_1
β' : Type ?u.1147241
γ : Type ?u.1147244
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x)}
α : Type u_2
α' : Type ?u.1147235
β : Type u_1
β' : Type ?u.1147241
γ : Type ?u.1147244
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | Integrable (f x)}
simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and_iff]
no goals
α : Type u_2
α' : Type ?u.1147235
β : Type u_1
β' : Type ?u.1147241
γ : Type ?u.1147244
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x)}
exact measurableSet_lt (Measurable.lintegral_prod_right hf.ennnorm) measurable_const