bUnion — Mathlib

English

If a family s(n) is independently from s' for every n in a subset u of indices, then the union over n in u of s(n) is independent from s'.

Русский

Если для каждого n из подмножества u семейство \$s(n)\$ независимо от \$s'\$, то объединение по всем n из u независимо от \$s'\$.

LaTeX

$$$\\Big( \\forall n \\in u, IndepSets(s(n), s'; \\mu) \\Big) \\Rightarrow IndepSets\\Big(\\bigcup_{n \\in u} s(n), s'; \\mu\\Big)$$$

Lean4

theorem bUnion {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (hyp : ∀ n ∈ u, IndepSets (s n) s' μ) :
    IndepSets (⋃ n ∈ u, s n) s' μ :=
  Kernel.IndepSets.bUnion hyp

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