α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
⊢ f - g =ᵐ[μ] 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
⊢ f =ᵐ[μ] g
rw [← sub_ae_eq_zero]
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, (f - g) x ∂μ) = 0
⊢ f - g =ᵐ[μ] 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
⊢ f - g =ᵐ[μ] 0
have hfg' : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
  intro s hs hμs
  rw [integral_sub' hf.integrableOn hg.integrableOn]
  exact sub_eq_zero.mpr (hfg s hs hμs)
no goals
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, (f - g) x ∂μ) = 0
⊢ f - g =ᵐ[μ] 0
exact Integrable.ae_eq_zero_of_forall_set_integral_eq_zero (hf.sub hg) hfg'
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (x : α) in s, (f - g) x ∂μ) = 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, (f - g) x ∂μ) = 0
intro s hs hμs
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ((∫ (a : α) in s, f a ∂μ) - ∫ (a : α) in s, g a ∂μ) = 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (x : α) in s, (f - g) x ∂μ) = 0
rw [integral_sub' hf.integrableOn hg.integrableOn]
no goals
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f g : α → E
hf : Integrable f
hg : Integrable g
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ((∫ (a : α) in s, f a ∂μ) - ∫ (a : α) in s, g a ∂μ) = 0
exact sub_eq_zero.mpr (hfg s hs hμs)