indep_iSup_of_disjoint — Mathlib

English

If m is directed across a family with disjoint index sets S and T, then the suprema over S and T are independent.

Русский

Если семейство индексов разбилось на два дизъюнктивных множества S и T и маппированное по ним пространство направлено на согласованные супремы, то полученные супремы независимы.

LaTeX

$$Indep(iSup_{i∈S} m_i, iSup_{i∈T} m_i; μ)$$

Lean4

theorem indep_iSup_of_disjoint (h_le : ∀ i, m i ≤ _mΩ) (h_indep : iIndep m μ) {S T : Set ι} (hST : Disjoint S T) :
    Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) μ :=
  Kernel.indep_iSup_of_disjoint h_le h_indep hST

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