Theorems · Theorem · measure theory

CompactlySupportedContinuousMap.integrable

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X] {E : Type u_2}
  [inst_3 : NormedAddCommGroup E] (f : CompactlySupportedContinuousMap X E) {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ], MeasureTheory.Integrable (⇑f) μ

Defined in

Mathlib.MeasureTheory.Integral.CompactlySupported

Cited by

9 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceNormedAddCommGroupMeasureTheory.IsFiniteMeasureOnCompacts