Theorems · Theorem · measure theory

intervalIntegral.integral_smul

∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ} [inst_2 : NormedDivisionRing 𝕜] [inst_3 : Module 𝕜 E] [NormSMulClass 𝕜 E]
  [SMulCommClass ℝ 𝕜 E] (r : 𝕜) (f : ℝ → E), ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ

Compatibility with scalar multiplication. Note this assumes 𝕜 is a division ring in order to ensure that for c ≠ 0, c • f is integrable iff f is. For scalar multiplication by more general rings assuming integrability, see IntervalIntegrable.integral_smul.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedDivisionRingModuleNormSMulClassSMulCommClass