theorem MeasureTheory.integral_eq_setIntegral {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ sᶜ = 0) (f : α → E) : ∫ (x : α), f x ∂μ = ∫ (x : α) in s, f x ∂μ