Integrals of continuous functions with respect to regular measures

When a measure is regular, one may express the measure of compact sets and of open sets in terms of the integral of continuous functions equal to 1 on the compact set, or to 0 outside of the open set respectively.

theorem IsCompact.measure_eq_biInf_integral_hasCompactSupport {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {k : Set X} (hk : IsCompact k) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] [LocallyCompactSpace X] [RegularSpace X] : μ k = ⨅ (f : X → ℝ), ⨅ (_ : 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.

theorem IsOpen.measure_eq_biSup_integral_continuous {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [T2Space X] {U : Set X} (hU : IsOpen U) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegularCompactLTTop] [NormalSpace X] : μ U = ⨆ (f : X → ℝ), ⨆ (_ : Continuous f), ⨆ (_ : Set.EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)

Given an inner regular finite measure, the measure of an open set is the supremum of the integrals of nonnegative continuous functions supported in this set and bounded by 1.