indep_iSup_of_directed_le — Mathlib

English

If m is directed and iIndep m μ, then the two directed suprema over S and T are independent.

Русский

Если m упорядочено направленно и iIndep m μ, то два направленных суприма независимы.

LaTeX

$$indep_iSup_of_directed_le ... Indep(iSup_{i} m_i, iSup_{i} m_i; μ)$$

Lean4

theorem indep_iSup_of_directed_le [IsZeroOrProbabilityMeasure μ] (h_indep : ∀ i, Indep (m i) m1 μ)
    (h_le : ∀ i, m i ≤ _mΩ) (h_le' : m1 ≤ _mΩ) (hm : Directed (· ≤ ·) m) : Indep (⨆ i, m i) m1 μ :=
  Kernel.indep_iSup_of_directed_le h_indep h_le h_le' hm

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