Theorems · Theorem · measure theory

CompactlySupportedContinuousMap.integralLinearMap_apply

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (μ : MeasureTheory.Measure X) [inst_3 : MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (f : CompactlySupportedContinuousMap X NNReal),
  (CompactlySupportedContinuousMap.integralLinearMap μ) f = NNReal.mk (∫ (x : X), ↑(f x) ∂μ) ⋯

Defined in

Mathlib.MeasureTheory.Integral.CompactlySupported

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasureOnCompacts