Theorems · Theorem · measure theory

integral_coe_re_add_coe_im

∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → 𝕜},
  MeasureTheory.Integrable f μ →
    ∫ (x : X), ↑(RCLike.re (f x)) ∂μ + (∫ (x : X), ↑(RCLike.im (f x)) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceRCLike