LeanMachineLearning exposition

ProbabilityTheory.indepFun_zero_measure🔗

Minimal Lean file

indepFun_zero_measure🔗

LemmaProbabilityTheory.indepFun_zero_measure
Details

No docstring.

🔗theorem
ProbabilityTheory.indepFun_zero_measure.{u_6, u_7, u_8} {α : Type u_6}
  {β : Type u_7} {γ : Type u_8} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (X : α → β)
  (Y : α → γ) : IndepFun X Y 0
ProbabilityTheory.indepFun_zero_measure.{u_6,
    u_7, u_8}
  {α : Type u_6} {β : Type u_7}
  {γ : Type u_8} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (X : α → β)
  (Y : α → γ) : IndepFun X Y 0

Code

lemma indepFun_zero_measure {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
    {mγ : MeasurableSpace γ} (X : α → β) (Y : α → γ) :
    X ⟂ᵢ[(0 : Measure α)] Y
Used by (1)

Actions: Source · Open Issue

Proof
by
  simp [indepFun_iff_measure_inter_preimage_eq_mul]