bUnion — Mathlib

English

If for all n in a finite index set u, CondIndepSets m' hm' (s n) s' μ, then CondIndepSets m' hm' (⋃ n ∈ u, s n) s' μ.

Русский

Если для всех n из конечного множества индексов u выполняется CondIndepSets m' hm' (s n) s' μ, то CondIndepSets m' hm' (⋃ n∈u, s n) s' μ.

LaTeX

$$$\\forall n \\in u, \\; CondIndepSets\\, m' hm' (s n) s' μ \\Rightarrow CondIndepSets\\, m' hm' (\\bigcup_{n\\in u} s_n) s' μ$$$

Lean4

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

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