iUnion — Mathlib

English

If every member s(n) is independent from s' with respect to μ, then the intersection over all n of s(n) is independent from s' with respect to μ.

Русский

Если каждый член \$s(n)\$ независим относительно \$s'\$ по μ, то пересечение всех \$s(n)\$ независимо от \$s'\$.

LaTeX

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

Lean4

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

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