Theorems · Theorem · probability

ProbabilityTheory.IndepSets.indep

∀ {Ω : Type u_1} {m1 m2 _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ] {p1 p2 : Set (Set Ω)},
  m1 ≤ _mΩ →
    m2 ≤ _mΩ →
      IsPiSystem p1 →
        IsPiSystem p2 →
          m1 = MeasurableSpace.generateFrom p1 →
            m2 = MeasurableSpace.generateFrom p2 → ProbabilityTheory.IndepSets p1 p2 μ → ProbabilityTheory.Indep m1 m2 μ

Defined in

Mathlib.Probability.Independence.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsZeroOrProbabilityMeasure