α : Type u_1
β : Type ?u.1518598
E : Type u_2
F : Type ?u.1518604
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ Integrable f
α : Type u_1
β : Type ?u.1518598
E : Type u_2
F : Type ?u.1518604
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ IntegrableOn f s
delta IntegrableOn
α : Type u_1
β : Type ?u.1518598
E : Type u_2
F : Type ?u.1518604
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ Integrable f
α : Type u_1
β : Type ?u.1518598
E : Type u_2
F : Type ?u.1518604
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ Integrable f
rw [Measure.restrict_add]
no goals
α : Type u_1
β : Type ?u.1518598
E : Type u_2
F : Type ?u.1518604
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ Integrable f
exact hμ.integrable.add_measure hν