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