Theorems · Definition · probability

ProbabilityTheory.Kernel.IndepSet

{α : Type u_1} →
  {Ω : Type u_2} →
    {_mα : MeasurableSpace α} →
      {_mΩ : MeasurableSpace Ω} →
        Set Ω →
          Set Ω →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.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.Kernel.Indep

Cited by

18 results in Mathlib

Foundations

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