Theorems · Theorem · measure theory

MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable

∀ {E : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace E] [inst_2 : PseudoEMetricSpace E]
  [BorelSpace E] [CompleteSpace E] [SecondCountableTopology E] {P P' : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P']
  {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)},
  (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints →
    (∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') → P = P'

If the integrals of all elements of a subalgebra A of continuous and bounded functions with respect to two finite measures P, P' coincide, then the measures coincide. In other words: If a subalgebra separates points, it separates finite measures.

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasureExt

Cited by

3 results in Mathlib

Foundations

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

Assumes

RCLikeMeasurableSpacePseudoEMetricSpaceBorelSpaceCompleteSpaceSecondCountableTopologyMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure