case pos
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : IntegrableOn f s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case neg
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : ¬IntegrableOn f s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ
by_cases hfi : IntegrableOn f s μ
case neg
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : ¬IntegrableOn f s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case pos
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : IntegrableOn f s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ
case pos
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : IntegrableOn f s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case neg
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : ¬IntegrableOn f s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ
swap
case neg
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : ¬IntegrableOn f s
⊢ ¬Integrable fun x => indicator s f x
case neg
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : ¬IntegrableOn f s
⊢ (∫ (x : α), indicator s f x ∂μ) = ∫ (x : α) in s, f x ∂μ
rwa [integral_undef, integral_undef]
no goals
case neg
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : ¬IntegrableOn f s
⊢ ¬Integrable fun x => indicator s f x
rwa [integrable_indicator_iff hs]
no goals
α : Type u_1
β : Type ?u.36984
E : Type u_2
F : Type ?u.36990
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hfi : IntegrableOn f s
⊢ ((∫ (x : α) in s, f x ∂μ) + ∫ (x : α) in sᶜ, 0 ∂μ) = ∫ (x : α) in s, f x ∂μ
simp