Theorems · Theorem · measure theory

MeasureTheory.integral_countable

∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {f : X → E}
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X} [Countable X],
  MeasureTheory.Integrable f μ → ∫ (x : X), f x ∂μ = ∑' (x : X), μ.real {x} • f x

Defined in

Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Cited by

3 results in Mathlib

Foundations

Depth 256 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSingletonClassCountable