Theorems · Theorem · measure theory

MeasureTheory.Measure.infinitePi_singleton_of_fintype

∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [inst : Fintype ι]
  [∀ (i : ι), MeasurableSingletonClass (X i)] (f : (i : ι) → X i),
  (MeasureTheory.Measure.infinitePi μ) {f} = ∏ i, (μ i) {f i}

Defined in

Mathlib.Probability.ProductMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureFintypeMeasurableSingletonClass