iIndepSet_of_mem — Mathlib

English

If the family of pi-systems is independent and the generating sigma-algebras satisfy the generator relation, then the induced iIndep holds for the whole index set.

Русский

Если семейство пи-систем независимо и порождающие сигма-алгебры удовлетворяют условию генератора, то получаем независимость для всего множества индексов.

LaTeX

$$$iIndep m κ μ$ given the assumptions on π and h_indepSets$$

Lean4

theorem iIndepSet_of_mem {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {π : ι → Set (Set Ω)}
    {f : ι → Set Ω} (hfπ : ∀ i, f i ∈ π i) (hf : ∀ i, MeasurableSet (f i)) (hπ : iIndepSets π κ μ) : iIndepSet f κ μ :=
  (iIndepSet_iff_meas_biInter hf).2 fun _t ↦ hπ.meas_biInter _ fun _i _ ↦ hfπ _

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