Theorems · Theorem · probability

ProbabilityTheory.IndepSets_iff

∀ {Ω : Type u_1} {x : MeasurableSpace Ω} (s1 s2 : Set (Set Ω)) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepSets s1 s2 μ ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ (t1 ∩ t2) = μ t1 * μ t2

Defined in

Mathlib.Probability.Independence.Basic

Cited by

3 results in Mathlib

Foundations

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