Theorems · Theorem · measure theory

MeasureTheory.measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω]
  [OpensMeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν) →
    ∀ {F : Set Ω}, IsClosed F → μ F = ν F

Two finite measures give equal values to all closed sets if the integrals of all bounded continuous functions with respect to the two measures agree.

Defined in

Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceHasOuterApproxClosedOpensMeasurableSpaceMeasureTheory.IsFiniteMeasure