iIndepFun_iff_finset — Mathlib

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

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