no goals
α : Type u
β : Type v
γ : Type ?u.38336
δ : Type ?u.38339
ε : Type ?u.38342
ζ : Type ?u.38345
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
a : α
b : β
⊢ s ×ˢ t ∈ 𝓝 (a, b) ↔ s ∈ 𝓝 a ∧ t ∈ 𝓝 b
rw [nhds_prod_eq, prod_mem_prod_iff]