iIndepSet_iff_meas_biInter — Mathlib

English

Independence of a finite family of sets f_i implies the product formula for their intersection: μ(⋂ i∈s f_i) = ∏ i∈s μ(f_i).

Русский

Независимость конечной семьи множеств f_i влечёт произведение меры на пересечение: μ(⋂ i∈s f_i) = ∏ i∈s μ(f_i).

LaTeX

$$$iIndepSet f μ \Rightarrow ∀ s, μ(⋂ i∈s f_i) = ∏ i∈s μ(f_i)$$$

Lean4

theorem iIndepSet_iff_meas_biInter {f : ι → Set Ω} (hf : ∀ i, MeasurableSet (f i)) :
    iIndepSet f μ ↔ ∀ s, μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i) := by
  simp_rw [iIndepSet, Kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

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