set_biInter_inter — Mathlib

English

Intersection over x in s ∪ t of u(x) equals intersection over x in s of u(x) and intersection over x in t of u(x).

Русский

Пересечение по x∈s∪t равно пересечению по x∈s и по x∈t совместно.

LaTeX

$$$$ \\bigcap_{x \\in s \\cup t} u(x) = \\left(\\bigcap_{x \\in s} u(x)\\right) \\cap \\left(\\bigcap_{x \\in t} u(x)\\right) $$$$

Lean4

theorem set_biInter_inter (s t : Finset α) (u : α → Set β) : ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x :=
  iInf_union

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