no goals
α : Type u
β : Type v
γ : Type ?u.34864
δ : Type ?u.34867
ε : Type ?u.34870
ζ : Type ?u.34873
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
s : Set (α × β)
⊢ s ∈ 𝓝 (a, b) ↔ ∃ u, u ∈ 𝓝 a ∧ ∃ v, v ∈ 𝓝 b ∧ u ×ˢ v ⊆ s
rw [nhds_prod_eq, mem_prod_iff]