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]