Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.ext_of_forall_integral_eq

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω]
  {μ ν : MeasureTheory.FiniteMeasure Ω},
  (∀ (f : BoundedContinuousFunction Ω ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν) → μ = ν

Two finite Borel measures are equal if the integrals of all bounded continuous functions with respect to both agree.

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceHasOuterApproxClosedBorelSpace