English
If a family of sigma-algebras (m_i) is increasing (monotone) and each m_i is independent of a fixed sigma-algebra m' with respect to κ and μ, and all m_i lie below a common bound m0, then the supremum of the m_i is independent of m'.
Русский
Если семейство сигма-алгебр (m_i) возрастает (монотонно), каждая m_i независима от фиксированной сигма-алгебры m' относительно κ и μ, и все m_i лежат ниже общей границы m0, тогда их объединение (предел supremum) независимо от m'.
LaTeX
$$$Indep\left(\bigvee_i m_i\right) m'\ κ\ μ$$$
Lean4
theorem indep_iSup_of_monotone [SemilatticeSup ι] {Ω} {m : ι → MeasurableSpace Ω} {m' m0 : MeasurableSpace Ω}
{κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ] (h_indep : ∀ i, Indep (m i) m' κ μ) (h_le : ∀ i, m i ≤ m0)
(h_le' : m' ≤ m0) (hm : Monotone m) : Indep (⨆ i, m i) m' κ μ :=
indep_iSup_of_directed_le h_indep h_le h_le' (Monotone.directed_le hm)
