bInter — Mathlib

English

If there exists n ∈ u with IndepSets(s_n) from s', then IndepSets(⋂ n ∈ u, s_n) from s' μ.

Русский

Если существует n ∈ u такое, что IndepSets(s_n, s'; μ), то IndepSets(⋂ n ∈ u, s_n, s'; μ).

LaTeX

$$$\\exists n \\in u, IndepSets(s_n, s'; \\mu) \\Rightarrow IndepSets(\\bigcap_{n \\in u} s_n, s'; \\mu)$$$

Lean4

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

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