iUnion — Mathlib

English

If each s_n is independent with s' then the union over n is independent with s'.

Русский

Если для каждого n множество s_n независимо от s', то объединение по n также независимо от s'.

LaTeX

$$$\\forall n, \\text{CondIndepSets}\, m' hm' (s_n) s' μ \\Rightarrow \\text{CondIndepSets}\, m' hm' (\\bigcup_n s_n) s' μ$$$

Lean4

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

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