English
Union over n of s(n.unpair.fst) × t(n.unpair.snd) equals the product of unions, i.e., (Union s) × (Union t).
Русский
Объединение по n от s(n.unpair.fst) × t(n.unpair.snd) равно произведению объединений, то есть (Union s) × (Union t).
LaTeX
$$$ \bigcup_{n \in \mathbb{N}}\big( s(\operatorname{fst}(\operatorname{unpair}(n))) \times t(\operatorname{snd}(\operatorname{unpair}(n))) \big) = \Big( \bigcup_{n} s(n) \Big) \times \Big( \bigcup_{n} t(n) \Big). $$$
Lean4
theorem iUnion_unpair_prod {α β} {s : ℕ → Set α} {t : ℕ → Set β} :
⋃ n : ℕ, s n.unpair.fst ×ˢ t n.unpair.snd = (⋃ n, s n) ×ˢ ⋃ n, t n :=
by
rw [← Set.iUnion_prod]
exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)
