Theorems · Theorem · measure theory

IntervalIntegrable.sum

∀ {ι : Type u_1} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ENormedAddCommMonoid ε] [ContinuousAdd ε] (s : Finset ι) {f : ι → ℝ → ε},
  (∀ i ∈ s, IntervalIntegrable (f i) μ a b) → IntervalIntegrable (∑ i ∈ s, f i) μ a b

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceENormedAddCommMonoidContinuousAdd