indep_generateFrom_lt — Mathlib

English

If hs is a family of measurable sets, hs is iIndepSet, and S,T are disjoint, then the generated indep structure over the corresponding unions is independent.

Русский

Если hs — семейство измеримых множеств и непересечение S и T, то порожденная независимость сохраняется.

LaTeX

$$ ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint (hs ae) (S,T,hST) : Indep (...)$$

Lean4

theorem indep_generateFrom_lt [Preorder ι] {s : ι → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s κ μ)
    (i : ι) : Indep (generateFrom {s i}) (generateFrom {t | ∃ j < i, s j = t}) κ μ :=
  by
  convert
    iIndepSet.indep_generateFrom_of_disjoint hsm hs { i } {j | j < i}
      (Set.disjoint_singleton_left.mpr (lt_irrefl _)) using
    1
  simp only [Set.mem_singleton_iff, exists_eq_left, Set.setOf_eq_eq_singleton']

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