Theorems · Theorem · measure theory

IntervalIntegrable.continuousOn_smul

∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → 𝕜}
  {g : ℝ → E} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [IsBoundedSMul 𝕜 E],
  IntervalIntegrable g μ a b → ContinuousOn f (Set.uIcc a b) → IntervalIntegrable (fun x => f x • g x) μ a b

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedRingModuleIsBoundedSMul