Theorems · Theorem · measure theory

Measure.ext_of_integral_prod_mul_boundedContinuousFunction

∀ {ι : Type u_1} {T : Type u_4} {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] [inst_6 : Fintype ι]
  {μ ν : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
        ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν) →
    μ = ν

Defined in

Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceBorelSpaceHasOuterApproxClosedFintypeMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure