Theorems · Theorem · measure theory

IntervalIntegrable.add

∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f g : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ} [ContinuousAdd ε],
  IntervalIntegrable f μ a b → IntervalIntegrable g μ a b → IntervalIntegrable (fun x => f x + g x) μ a b

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceENormedAddMonoidContinuousAdd