Theorems · Theorem · measure theory

MeasureTheory.Measure.pi_eq_generateFrom

∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} {C : (i : ι) → Set (Set (α i))},
  (∀ (i : ι), MeasurableSpace.generateFrom (C i) = inst_1 i) →
    (∀ (i : ι), IsPiSystem (C i)) →
      ∀ (h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)) {μν : MeasureTheory.Measure ((i : ι) → α i)},
        (∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (Set.univ.pi s) = ∏ i, (μ i) (s i)) →
          MeasureTheory.Measure.pi μ = μν

A measure on a finite product space equals the product measure if they are equal on rectangles with as sides sets that generate the corresponding σ-algebras.

Defined in

Mathlib.MeasureTheory.Constructions.Pi

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeMeasurableSpace