theorem MeasureTheory.integral_eq_sum {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasurableSingletonClass α] [Fintype α] (f : α → E) : ∫ (x : α), f x ∂μ = Finset.univ.sum fun (x : α) => (μ {x}).toReal • f x