set_biInter_biUnion — Mathlib

English

The intersection over y in s.biUnion t of f(y) equals the intersection over x in s and y in t(x) of f(y).

Русский

Пересечение по y в s.biUnion t равно пересечению по x в s и y в t(x) от f(y).

LaTeX

$$$$ \\bigcap_{y \\in s.biUnion t} f(y) = \\bigcap_{x \\in s} \\bigcap_{y \\in t(x)} f(y) $$$$

Lean4

theorem set_biInter_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → Set β) :
    ⋂ y ∈ s.biUnion t, f y = ⋂ (x ∈ s) (y ∈ t x), f y :=
  iInf_biUnion s t f

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