condIndep_generateFrom_le — Mathlib

English

If m is antitone and each i yields CondIndep m' (m i) m₁ hm' μ, then CondIndep m' (iSup i m_i) m₁ hm' μ.

Русский

Если mAntitone и каждый i даёт CondIndep m' (m_i) m₁ hm' μ, тогда CondIndep m' (iSup_i m_i) m₁ hm' μ.

LaTeX

$$$\mathrm{CondIndep}(m', \bigvee_i m_i, m_1, hm', \mu)$$$

Lean4

theorem condIndep_generateFrom_le [Preorder ι] {s : ι → Set Ω} (hsm : ∀ n, MeasurableSet (s n))
    (hs : iCondIndepSet m' hm' s μ) (i : ι) {k : ι} (hk : i < k) :
    CondIndep m' (generateFrom {s k}) (generateFrom {t | ∃ j ≤ i, s j = t}) hm' μ :=
  Kernel.iIndepSet.indep_generateFrom_le hsm hs i hk

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