α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
let k := f ⁻¹' {0}
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MeasurableSet k
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
⊢ MeasurableSet k
borelize E
no goals
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MeasurableSet k
exact haux.measurable (measurableSet_singleton _)
no goals
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ (∫ (x : α) in t, f x ∂μ) = (∫ (x : α) in t ∩ k, f x ∂μ) + ∫ (x : α) in t \ k, f x ∂μ
rw [integral_inter_add_diff hk h'aux]
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t ∩ k
⊢ f x = 0
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ((∫ (x : α) in t ∩ k, f x ∂μ) + ∫ (x : α) in t \ k, f x ∂μ) = ∫ (x : α) in t \ k, f x ∂μ
rw [set_integral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]
no goals
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t ∩ k
⊢ f x = 0
exact hx.2
case hst
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ t \ k =ᵐ[μ] s \ k
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ (∫ (x : α) in t \ k, f x ∂μ) = ∫ (x : α) in s \ k, f x ∂μ
apply set_integral_congr_set_ae
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
⊢ (t \ f ⁻¹' {0}) x = (s \ f ⁻¹' {0}) x
case hst
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ t \ k =ᵐ[μ] s \ k
filter_upwards [h't] with x hx
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
⊢ (x ∈ t \ k) = (x ∈ s \ k)
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
⊢ (t \ f ⁻¹' {0}) x = (s \ f ⁻¹' {0}) x
change (x ∈ t \ k) = (x ∈ s \ k)
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
⊢ ¬f x = 0 → (x ∈ t ↔ x ∈ s)
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
⊢ (x ∈ t \ k) = (x ∈ s \ k)
simp only [mem_preimage, mem_singleton_iff, eq_iff_iff, and_congr_left_iff, mem_diff]
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
⊢ x ∈ t ↔ x ∈ s
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
⊢ ¬f x = 0 → (x ∈ t ↔ x ∈ s)
intro h'x
case pos
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : x ∈ s
⊢ x ∈ t ↔ x ∈ s

case neg
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : ¬x ∈ s
⊢ x ∈ t ↔ x ∈ s
case h
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
⊢ x ∈ t ↔ x ∈ s
by_cases xs : x ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : x ∈ s
⊢ x ∈ t ↔ x ∈ s
simp only [xs, hts xs]
case neg
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : ¬x ∈ s
⊢ ¬x ∈ t
case neg
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : ¬x ∈ s
⊢ x ∈ t ↔ x ∈ s
simp only [xs, iff_false_iff]
case neg
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : ¬x ∈ s
xt : x ∈ t
⊢ False
case neg
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : ¬x ∈ s
⊢ ¬x ∈ t
intro xt
no goals
case neg
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
x : α
hx : x ∈ t \ s → f x = 0
h'x : ¬f x = 0
xs : ¬x ∈ s
xt : x ∈ t
⊢ False
exact h'x (hx ⟨xt, xs⟩)
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
this : ∀ (x : α), x ∈ s ∩ k → f x = 0
⊢ (∫ (x : α) in s \ k, f x ∂μ) = (∫ (x : α) in s ∩ k, f x ∂μ) + ∫ (x : α) in s \ k, f x ∂μ
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ (∫ (x : α) in s \ k, f x ∂μ) = (∫ (x : α) in s ∩ k, f x ∂μ) + ∫ (x : α) in s \ k, f x ∂μ
have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
no goals
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
this : ∀ (x : α), x ∈ s ∩ k → f x = 0
⊢ (∫ (x : α) in s \ k, f x ∂μ) = (∫ (x : α) in s ∩ k, f x ∂μ) + ∫ (x : α) in s \ k, f x ∂μ
rw [set_integral_eq_zero_of_forall_eq_zero this, zero_add]
no goals
α : Type u_1
β : Type ?u.88408
E : Type u_2
F : Type ?u.88414
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ((∫ (x : α) in s ∩ k, f x ∂μ) + ∫ (x : α) in s \ k, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]