biUnion_iUnion — Mathlib

English

For sets s : ι → Set α and t : α → Set β, the union over x in ⋃ i, s i of t x equals the union over i and x ∈ s i of t x.

Русский

Для множеств s : ι → Set α и t : α → Set β объединение по x из ⋃ i, s i множества t x равно объединению по i и по x ∈ s i множества t x.

LaTeX

$$$$ \\bigcup_{x \\in \\bigcup_i s_i} t(x) = \\bigcup_{i} \\bigcup_{x \\in s_i} t(x). $$$$

Lean4

theorem biUnion_iUnion (s : ι → Set α) (t : α → Set β) : ⋃ x ∈ ⋃ i, s i, t x = ⋃ (i) (x ∈ s i), t x := by
  simp [@iUnion_comm _ ι]

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