Theorems · Theorem · probability

ProbabilityTheory.iIndep_iff_iIndepSets

∀ {Ω : Type u_1} {ι : Type u_2} (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndep m μ ↔ ProbabilityTheory.iIndepSets (fun x => {s | MeasurableSet s}) μ

Defined in

Mathlib.Probability.Independence.Basic

Cited by

1 results in Mathlib

Foundations

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