iInter — Mathlib

English

If there exists an index n with IndepSets(s_n) from s' μ, then the intersection over all n of s_n is independent from s'.

Русский

Если существует индекс n такой, что \$IndepSets(s_n, s'; \\mu)\$, тогда пересечение по всем n независимо от \$s'\$.

LaTeX

$$$\\exists n, IndepSets(s_n, s'; \\mu) \\Rightarrow IndepSets(\\bigcap_n s_n, s'; \\mu)$$$

Lean4

theorem iInter {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} (h : ∃ n, IndepSets (s n) s' μ) : IndepSets (⋂ n, s n) s' μ :=
  Kernel.IndepSets.iInter h

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