iIndep_iff_iIndepSets — Mathlib

English

Independence of a family is equivalent to independence of the corresponding family of events.

Русский

Независимость семейства эквивалентна независимости соответствующего семейства событий.

LaTeX

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

Lean4

theorem iIndep_iff_iIndepSets (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    iIndep m μ ↔ iIndepSets (fun x ↦ {s | MeasurableSet[m x] s}) μ := by simp only [iIndep, iIndepSets, Kernel.iIndep]

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