English
The image under a function of a biUnion over a product equals a nested iUnion of images over the product indices.
Русский
Образ под функцией биобъединения над произведением равен вложенному iUnion образов по индексам.
LaTeX
$$$\bigcup_{x \in s \times t} f(x) = \bigcup_{i \in s} \bigcup_{j \in t} f(i,j)$$$
Lean4
theorem biUnion_prod {α β γ} (s : Set α) (t : Set β) (f : α → Set γ) (g : β → Set δ) :
⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ (⋃ x ∈ t, g x) :=
by
ext ⟨_, _⟩
simp only [mem_iUnion, mem_prod, exists_prop, Prod.exists]; tauto