α : Type u_1
β : Type ?u.1499967
E : Type u_2
F : Type ?u.1499973
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h : IntegrableOn f s
hs : MeasurableSet s
⊢ Integrable f
α : Type u_1
β : Type ?u.1499967
E : Type u_2
F : Type ?u.1499973
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h : IntegrableOn f s
hs : MeasurableSet s
⊢ IntegrableOn f s
rw [IntegrableOn, Measure.restrict_restrict hs]
no goals
α : Type u_1
β : Type ?u.1499967
E : Type u_2
F : Type ?u.1499973
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h : IntegrableOn f s
hs : MeasurableSet s
⊢ Integrable f
exact h.mono_set (inter_subset_left _ _)