iIndepFun_iff_iIndep — Mathlib

English

For families of measurable spaces (β_i) and measurable maps f_i: Ω → β_i, the independence of f_i with respect to μ is equivalent to the independence of the pullback sigma-algebras via f_i.

Русский

Для семей измеримых пространств β_i и измеримых отображений f_i: Ω → β_i независимость набора функций f_i относительно μ эквивалентна независимости соответствующих обратно-потянутых сигма-алгебр через f_i.

LaTeX

$$$\text{iIndepFun}(f,\mu) \iff \text{Indep}\bigl(i \mapsto (m_i).\text{comap}(f_i)\bigr)\mu$$$

Lean4

theorem iIndepFun_iff_iIndep {β : ι → Type*} (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x)
    (μ : Measure Ω) : iIndepFun f μ ↔ iIndep (fun x ↦ (m x).comap (f x)) μ := by
  simp only [iIndepFun, iIndep, Kernel.iIndepFun]

Похожие утверждения