condIndep_iSup_of_antitone — Mathlib

English

If for every i, CondIndep m' hm' m_i hm' μ holds, and m is monotone, then CondIndep m' (iSup_i m_i) m₁ hm' μ holds.

Русский

Если для каждого i верна CondIndep m' hm' m_i hm' μ и если m монотонно возрастает, то CondIndep между iSup и m₁ держится.

LaTeX

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

Lean4

theorem condIndep_iSup_of_antitone [SemilatticeInf ι] {m : ι → MeasurableSpace Ω}
    (h_indep : ∀ i, CondIndep m' (m i) m₁ hm' μ) (h_le : ∀ i, m i ≤ mΩ) (h_le' : m₁ ≤ mΩ) (hm : Antitone m) :
    CondIndep m' (⨆ i, m i) m₁ hm' μ :=
  Kernel.indep_iSup_of_antitone h_indep h_le h_le' hm

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