Theorems · Definition · probability

ProbabilityTheory.iIndepSets

{Ω : Type u_1} →
  {ι : Type u_2} →
    {_mΩ : MeasurableSpace Ω} →
      (ι → Set (Set Ω)) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iIndepSets._auto_1 → Prop

A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ π i_1, ..., f i_n ∈ π i_n, then μ (⋂ i in s, f i) = ∏ i ∈ s, μ (f i) . It will be used for families of π-systems.

Defined in

Mathlib.Probability.Independence.Basic

Cited by

18 results in Mathlib

Foundations

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