Theorems · Theorem · measure theory

BoundedContinuousFunction.integral_add_const

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

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