case hμ
α : Type u_1
β : Type ?u.8904
E : Type u_2
F : Type ?u.8910
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hfs : IntegrableOn f s
⊢ Integrable fun x => f x

case hν
α : Type u_1
β : Type ?u.8904
E : Type u_2
F : Type ?u.8910
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hfs : IntegrableOn f s
⊢ Integrable fun x => f x
α : Type u_1
β : Type ?u.8904
E : Type u_2
F : Type ?u.8910
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hfs : IntegrableOn f s
⊢ ((∫ (x : α) in s ∩ t, f x ∂μ) + ∫ (x : α) in s \ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
rw [← Measure.restrict_inter_add_diff₀ s ht, integral_add_measure]
no goals
case hμ
α : Type u_1
β : Type ?u.8904
E : Type u_2
F : Type ?u.8910
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hfs : IntegrableOn f s
⊢ Integrable fun x => f x
exact Integrable.mono_measure hfs (Measure.restrict_mono (inter_subset_left _ _) le_rfl)
no goals
case hν
α : Type u_1
β : Type ?u.8904
E : Type u_2
F : Type ?u.8910
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hfs : IntegrableOn f s
⊢ Integrable fun x => f x
exact Integrable.mono_measure hfs (Measure.restrict_mono (diff_subset _ _) le_rfl)