Theorems · Theorem · measure theory

Measure.ext_of_integral_mul_prod_boundedContinuousFunction

∀ {κ : Type u_2} {Z : Type u_3} {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)}
  [inst : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)]
  {mZ : MeasurableSpace Z} [inst_3 : TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] [inst_6 : Fintype κ]
  {μ ν : MeasureTheory.Measure (Z × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ),
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ =
        ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ν) →
    μ = ν

Defined in

Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceBorelSpaceHasOuterApproxClosedFintypeMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure