English
An equality exchanging iUnion and cartesian product holds: ⋃ x, s x × t x equals (⋃ x, s x) × (⋃ x, t x).
Русский
Справедливо равенство, меняющее iUnion и произведение: ⋃ x, s(x) × t(x) = (⋃ x, s(x)) × (⋃ x, t(x)).
LaTeX
$$$\bigcup_{x} (s_x \times t_x) = (\bigcup_x s_x) \times (\bigcup_x t_x)$$$
Lean4
theorem iUnion_prod {ι ι' α β} (s : ι → Set α) (t : ι' → Set β) :
⋃ x : ι × ι', s x.1 ×ˢ t x.2 = (⋃ i : ι, s i) ×ˢ ⋃ i : ι', t i :=
by
ext
simp