Theorems · Theorem · measure theory

ContinuousLinearMap.intervalIntegral_apply

∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure ℝ} [inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {a b : ℝ} {φ : ℝ → F →L[𝕜] E},
  IntervalIntegrable φ μ a b → ∀ (v : F), (∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceRCLikeNormedSpaceNormedAddCommGroupNormedSpace