indep_iSup_of_monotone — Mathlib

English

Another form: if h_indep holds for all i and m is monotone, then iSup of m_i is independent of m1.

Русский

Другая форма: если независимость для каждого i и монотонность m, тогда iSup модуля независим от m1.

LaTeX

$$[IsZeroOrProbabilityMeasure μ] ∀ i, Indep (m i) m1 μ → (Monotone m) ⇒ Indep (iSup i m i) m1 μ$$

Lean4

theorem indep_iSup_of_monotone [SemilatticeSup ι] [IsZeroOrProbabilityMeasure μ] (h_indep : ∀ i, Indep (m i) m1 μ)
    (h_le : ∀ i, m i ≤ _mΩ) (h_le' : m1 ≤ _mΩ) (hm : Monotone m) : Indep (⨆ i, m i) m1 μ :=
  Kernel.indep_iSup_of_monotone h_indep h_le h_le' hm

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