Theorems · Theorem · measure theory

intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm

∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [Countable ι]
  {f : ι → C(ℝ, E)},
  (Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖) →
    ∑' (i : ι), ∫ (x : ℝ) in a..b, (f i) x = ∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCountable