set_biUnion_coe — Mathlib

English

Let s be a finite set of elements of α and t a family of sets t(x) indexed by α. The union taken over the elements of the underlying set of s is the same as the union taken over the indices in s:

Русский

Пусть s — конечный набор элементов α, и t(x) — семейство множеств, индексируемое x из α. Объединение по элементам множества, переходящим в ↑s, равно объединению по индексам x∈s.

LaTeX

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

Lean4

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

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