Theorems · Theorem · probability

ProbabilityTheory.iIndepFun.meas_biInter

∀ {Ω : Type u_1} {ι : Type u_2} {κ : ι → Type u_5} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Finset ι}
  {s : ι → Set Ω} {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ω → κ x},
  ProbabilityTheory.iIndepFun f μ → (∀ i ∈ S, MeasurableSet (s i)) → μ (⋂ i ∈ S, s i) = ∏ i ∈ S, μ (s i)

Defined in

Mathlib.Probability.Independence.Basic

Cited by

1 results in Mathlib

Foundations

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