no goals
α : Type u_2
E : Type u_1
F : Type ?u.178579
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s : Set E
⊢ (⨍ (x : α), 0 ∂μ) = 0
rw [average, integral_zero]