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 _ ι]