Theorems · Theorem · probability

ProbabilityTheory.iIndepFun.hasLaw_pi

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_3} [inst : Fintype ι]
  {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {μ : (i : ι) → MeasureTheory.Measure (𝓧 i)}
  {X : (i : ι) → Ω → 𝓧 i},
  (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) →
    ProbabilityTheory.iIndepFun X P → ProbabilityTheory.HasLaw (fun ω i => X i ω) (MeasureTheory.Measure.pi μ) P

Defined in

Mathlib.Probability.HasLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

Fintype