bInter — Mathlib

English

There is a bInter version: if there exists n ∈ u with independence, then the intersection over n ∈ u of s n is independent from s'.

Русский

Существование независимости для некоторого n в u имплицитно даёт независимость пересечения по всем n∈u.

LaTeX

$$$\\exists n\\in u, CondIndepSets m' hm' (s n) s' μ \\Rightarrow CondIndepSets m' hm' (\\bigcap_{n∈u} s_n) s' μ$$$

Lean4

theorem bInter {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (h : ∃ n ∈ u, CondIndepSets m' hm' (s n) s' μ) :
    CondIndepSets m' hm' (⋂ n ∈ u, s n) s' μ :=
  Kernel.IndepSets.bInter h

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