Theorems · Theorem · probability

ProbabilityTheory.indep_iSup_of_antitone

∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {m1 _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeInf ι] [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  (∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) →
    (∀ (i : ι), m i ≤ _mΩ) → m1 ≤ _mΩ → Antitone m → ProbabilityTheory.Indep (⨆ i, m i) m1 μ

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

SemilatticeInfMeasureTheory.IsZeroOrProbabilityMeasure