English
If two families of functions are a.e.-equal termwise, then their iIndepFun properties are equivalent.
Русский
Если две семейства функций совпадают почти в каждой точке по каждой координате, то их свойства независимости сохраняются.
LaTeX
$$$iIndepFun f κ μ \Leftrightarrow iIndepFun g κ μ$ when f_i =ᵐ g_i a.e. for all i.$$
Lean4
theorem comp {β γ : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)} {mγ : ∀ i, MeasurableSpace (γ i)} {f : ∀ i, Ω → β i}
(h : iIndepFun f κ μ) (g : ∀ i, β i → γ i) (hg : ∀ i, Measurable (g i)) : iIndepFun (fun i ↦ g i ∘ f i) κ μ :=
by
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h ⊢
refine fun t s hs ↦ ?_
have := h t (sets := fun i ↦ g i ⁻¹' (s i)) (fun i a ↦ hg i (hs i a))
filter_upwards [this] with a ha
simp_rw [Set.preimage_comp]
exact ha
