set_biInter_insert — Mathlib

English

Inserting a into a finite set and taking intersections distributes as t(a) intersected with the intersection over s.

Русский

При вставке элемента a в конечное множество и взятии пересечений распределение выполняется как t(a) ∩ ⋂_{x∈s} t(x).

LaTeX

$$$$ \\bigcap_{x \\in \\operatorname{insert} a s} t(x) = t(a) \\cap \\bigcap_{x \\in s} t(x) $$$$

Lean4

theorem set_biInter_insert (a : α) (s : Finset α) (t : α → Set β) : ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x :=
  iInf_insert a s t

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