indep_biSup_compl — Mathlib

English

If a family s_n is independent in a kernel, then the independence holds between the supremum over a set t and the supremum over its complement tᶜ.

Русский

Если семейство s_n независимо в ядре, то независимость сохраняется между верхушкой над t и верхушкой над его комплементом.

LaTeX

$$$\\text{Indep}\\left(\\bigvee_{n\\in t} s_n, \\bigvee_{n\\in t^c} s_n\\right)\\kappa\\mu$$$

Lean4

theorem indep_biSup_compl (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s μ) (t : Set ι) :
    Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) μ :=
  Kernel.indep_biSup_compl h_le h_indep t

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