theorem MeasureTheory.lintegral_eq_sum {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (f : α → ENNReal) [Fintype α] : ∫⁻ (x : α), f x ∂μ = Finset.univ.sum fun (x : α) => μ {x} * f x

theorem MeasureTheory.lintegral_eq_sum_countable {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (f : α → ENNReal) [Countable α] : ∫⁻ (x : α), f x ∂μ = ∑' (x : α), μ {x} * f x

theorem MeasureTheory.lintegral_eq_zero_of_ae_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} {E : Set α} (hE : μ Eᶜ = 0) (hf : ∀ x ∈ E, f x = 0) (hmes : MeasurableSet E) : ∫⁻ (x : α), f x ∂μ = 0

theorem MeasureTheory.lintegral_eq_sum' {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) {s : Finset α} (hA : μ (↑s)ᶜ = 0) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = s.sum fun (x : α) => f x * μ {x}

theorem MeasureTheory.lintegral_eq_single {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (a : α) (f : α → ENNReal) (ha : ∀ (b : α), b ≠ a → f b = 0) : ∫⁻ (x : α), f x ∂μ = f a * μ {a}