theorem MeasuresAndSigmaAlgebras.rieszMeasure_isBorelMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [LocallyCompactSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) : borel X ≤ (RealRMK.rieszMeasure Λ).caratheodory

The Riesz representation measure of a positive linear functional on compactly supported continuous functions is a Borel measure: every Borel set is Caratheodory measurable with respect to its outer measure.

theorem MeasuresAndSigmaAlgebras.rieszMeasureC0_isBorelMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [LocallyCompactSpace X] (Λ : ZeroAtInftyContinuousMap X ℝ →ₗ[ℝ] ℝ) (hΛ : ∀ (f : ZeroAtInftyContinuousMap X ℝ), (∀ (x : X), 0 ≤ f x) → 0 ≤ Λ f) : borel X ≤ (rieszMeasureOfC0Functional Λ hΛ).caratheodory

The Riesz representation measure associated to a positive linear functional on C₀(X, ℝ) is a Borel measure.