α : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
f✝ : α → E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f
hf_int : (∫ (x : α), inner (∫ (x : α), f x ∂μ) (f x) ∂μ) = 0
⊢ (∫ (x : α), f x ∂μ) = 0
α : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
f✝ : α → E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f
hf_int : ∀ (c : E), (∫ (x : α), inner c (f x) ∂μ) = 0
⊢ (∫ (x : α), f x ∂μ) = 0
specialize hf_int (∫ x, f x ∂μ)
no goals
α : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
f✝ : α → E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f
hf_int : (∫ (x : α), inner (∫ (x : α), f x ∂μ) (f x) ∂μ) = 0
⊢ (∫ (x : α), f x ∂μ) = 0
rwa [integral_inner hf, inner_self_eq_zero] at hf_int