α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ (⋃ (n : ℕ), s (unpair n).fst ×ˢ t (unpair n).snd) = ⋃ (x : ℕ × ℕ), s x.fst ×ˢ t x.snd
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ (⋃ (n : ℕ), s (unpair n).fst ×ˢ t (unpair n).snd) = (⋃ (n : ℕ), s n) ×ˢ ⋃ (n : ℕ), t n
rw [← Set.iUnion_prod]
no goals
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ (⋃ (n : ℕ), s (unpair n).fst ×ˢ t (unpair n).snd) = ⋃ (x : ℕ × ℕ), s x.fst ×ˢ t x.snd
exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)