Theorems · Theorem · probability

ProbabilityTheory.Indep_iff

∀ {Ω : Type u_1} (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.Indep m₁ m₂ μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Defined in

Mathlib.Probability.Independence.Basic

Cited by

2 results in Mathlib

Foundations

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