Theorems · Theorem · measure theory

Measure.ext_of_integral_mul_boundedContinuousFunction

∀ {Z : Type u_3} {T : Type u_4} {mZ : MeasurableSpace Z} [inst : TopologicalSpace Z] [BorelSpace Z]
  [HasOuterApproxClosed Z] {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T]
  [HasOuterApproxClosed T] {μ ν : MeasureTheory.Measure (Z × T)} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν) →
    μ = ν

A finite measure μ over X × Y is determined by the values ∫ p, f p.1 * g p.2 ∂μ, for f : X → ℝ and g : Y → ℝ any bounded continuous functions.

Defined in

Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure