α : Type u_1
β : Type ?u.99624
E : Type u_2
F : Type ?u.99630
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
h : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ (∫ (x : α), f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.99624
E : Type u_2
F : Type ?u.99630
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
h : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α), f x ∂μ
symm
α : Type u_1
β : Type ?u.99624
E : Type u_2
F : Type ?u.99630
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
h : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ (∫ (x : α) in univ, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.99624
E : Type u_2
F : Type ?u.99630
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
h : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ (∫ (x : α), f x ∂μ) = ∫ (x : α) in s, f x ∂μ
nth_rw 1 [← integral_univ]
α : Type u_1
β : Type ?u.99624
E : Type u_2
F : Type ?u.99630
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
h : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
α : Type u_1
β : Type ?u.99624
E : Type u_2
F : Type ?u.99630
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
h : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ (∫ (x : α) in univ, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
apply set_integral_eq_of_subset_of_ae_diff_eq_zero nullMeasurableSet_univ (subset_univ _)
no goals
α : Type u_1
β : Type ?u.99624
E : Type u_2
F : Type ?u.99630
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
h : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
filter_upwards [h] with x hx h'x using hx h'x.2