Theorems · Theorem · measure theory

BoundedContinuousFunction.integral_const_sub

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ℝ) (c : ℝ),
  ∫ (x : X), (BoundedContinuousFunction.const X c - f) x ∂μ = μ.real Set.univ • c - ∫ (x : X), f x ∂μ

Defined in

Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasure