Theorems · Definition · measure theory

CompactlySupportedContinuousMap.integralPositiveLinearMap

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    [inst_1 : MeasurableSpace X] →
      [OpensMeasurableSpace X] →
        (μ : MeasureTheory.Measure X) →
          [MeasureTheory.IsFiniteMeasureOnCompacts μ] → CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ

Integral as a positive linear functional on C_c(X, ℝ).

Defined in

Mathlib.MeasureTheory.Integral.CompactlySupported

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasureOnCompacts