English
An i-independence statement is equivalent to independence for all finite index sets under restriction.
Русский
Утверждение о i-независимости эквивалентно независимости для всех конечно-масштабируемых наборов через ограничение.
LaTeX
$$$ \\operatorname{iIndepFun} f μ \\iff ∀ S : Finset\, ι, \\operatorname{iIndepFun} (S.restrict f) μ$$$
Lean4
theorem iIndepFun_iff_finset : iIndepFun f μ ↔ ∀ s : Finset ι, iIndepFun (s.restrict f) μ
where
mp h s := h.precomp (g := ((↑) : s → ι)) Subtype.val_injective
mpr
h := by
rw [iIndepFun_iff]
intro s f hs
have : ⋂ i ∈ s, f i = ⋂ i : s, f i := by ext; simp
rw [← Finset.prod_coe_sort, this]
exact (h s).meas_iInter fun i ↦ hs i i.2