Theorems · Definition · probability

ProbabilityTheory.IndepSet

{Ω : Type u_1} →
  {_mΩ : MeasurableSpace Ω} →
    Set Ω → Set Ω → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IndepSet._auto_1 → Prop

Two sets are independent if the two measurable space structures they generate are independent. For a set s, the generated measurable space structure has measurable sets ∅, s, sᶜ, univ.

Defined in

Mathlib.Probability.Independence.Basic

Cited by

13 results in Mathlib

Foundations

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