Theorems · Theorem · measure theory

intervalIntegral.intervalIntegral_re

∀ {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b → ∫ (x : ℝ) in a..b, RCLike.re (f x) ∂μ = RCLike.re (∫ (x : ℝ) in a..b, f x ∂μ)

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

RCLike