iIndepSet_iff_iIndepSets_singleton

English

For a family f, iIndepSet f μ is equivalent to iIndepSets of singleton sets {f_i} with each f_i measurable.

Русский

Для семейства f независимость iIndepSet эквивалентна независимости iIndepSets от множеств {f_i}, если все f_i измеримы.

LaTeX

$$$iIndepSet f μ \iff iIndepSets(\lambda i, {f_i}) μ$$

Lean4

theorem iIndepSet_iff_iIndepSets_singleton {f : ι → Set Ω} (hf : ∀ i, MeasurableSet (f i)) :
    iIndepSet f μ ↔ iIndepSets (fun i ↦ {f i}) μ :=
  Kernel.iIndepSet_iff_iIndepSets_singleton hf

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