Theorems · Theorem · measure theory

CompactlySupportedContinuousMap.integralPositiveLinearMap_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 ℝ),
  (CompactlySupportedContinuousMap.integralPositiveLinearMap μ) f = ∫ (x : X), f x ∂μ

Defined in

Mathlib.MeasureTheory.Integral.CompactlySupported

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasureOnCompacts