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

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