Theorems · Theorem · measure theory

IsCompact.measure_eq_biInf_integral_hasCompactSupport

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] {k : Set X},
  IsCompact k →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop]
      [LocallyCompactSpace X] [RegularSpace X],
      μ k =
        ⨅ f,
          ⨅ (_ : Continuous f),
            ⨅ (_ : HasCompactSupport f), ⨅ (_ : Set.EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)

In a locally compact regular space with an inner regular measure, the measure of a compact set k is the infimum of the integrals of compactly supported functions equal to 1 on k.

Defined in

Mathlib.MeasureTheory.Integral.Regular

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.InnerRegularCompactLTTopLocallyCompactSpaceRegularSpace