Theorems · Theorem · probability

ProbabilityTheory.IndepFun_iff

∀ {Ω : Type u_1} {x : MeasurableSpace Ω} {β : Type u_7} {γ : Type u_8} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
  (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepFun f g μ ↔ ∀ (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 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpace