iIndep_iff — Mathlib

English

A family is independent iff the corresponding family of measurable sets form an independence system.

Русский

Семейство независимо тогда, когда соответствующее семейство измеримых множеств образует систему независимости.

LaTeX

$$$iIndep m μ \iff iIndepSets (\lambda x. {S | MeasurableSet[S]}) μ$$

Lean4

theorem iIndep_iff (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    iIndep m μ ↔
      ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[m i] (f i)),
        μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i) :=
  by simp only [iIndep_iff_iIndepSets, iIndepSets_iff]; rfl

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