α✝ : Type ?u.22982
β✝ : Type ?u.22985
γ : Type ?u.22988
δ : Type ?u.22991
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
α✝ : Type ?u.22982
β✝ : Type ?u.22985
γ : Type ?u.22988
δ : Type ?u.22991
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)
rw [nhdsWithin_prod_eq]
no goals
α✝ : Type ?u.22982
β✝ : Type ?u.22985
γ : Type ?u.22988
δ : Type ?u.22991
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
exact prod_mem_prod hu hv