Theorems · Theorem · measure theory

intervalIntegral.intervalIntegral_conj

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

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLike