set_biInter_coe — Mathlib

English

Similar to the union case, the intersection over the underlying set of s equals the intersection over the finite index set s:

Русский

Аналогично случаю объединения, пересечение по элементам базового множества s равно пересечению по индексам x∈s.

LaTeX

$$$$ \\bigcap_{x \\in (\\uparrow s : \\mathrm{Set}\\, \\alpha)} t(x) = \\bigcap_{x \\in s} t(x) $$$$

Lean4

theorem set_biInter_coe (s : Finset α) (t : α → Set β) : ⋂ x ∈ (↑s : Set α), t x = ⋂ x ∈ s, t x :=
  rfl

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