English
iCondIndepFun_iff_iCondIndep: independence of a family of random mappings f,g is equivalent to independence after applying comaps to their codomains.
Русский
Независимость семейства отображений в условном смысле равна независимости после приложения компаков к их кодомандам.
LaTeX
$$$iCondIndepFun(m', hm', f, g, μ) \\iff iCondIndep(m', hm', (\\lambda x. \\mathrm{MeasurableSpace.comap}(f x) (m x)), μ)$$$
Lean4
theorem iCondIndepFun_iff_iCondIndep {β : ι → Type*} (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x)
(μ : Measure Ω) [IsFiniteMeasure μ] :
iCondIndepFun m' hm' f μ ↔ iCondIndep m' hm' (fun x ↦ MeasurableSpace.comap (f x) (m x)) μ := by
simp only [iCondIndepFun, iCondIndep, Kernel.iIndepFun]