no goals
α : Type u
β : Type v
γ : Type ?u.59142
δ : Type ?u.59145
ε : Type ?u.59148
ζ : Type ?u.59151
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ closure (s ×ˢ t) ↔ (a, b) ∈ closure s ×ˢ closure t
simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]