α : Type u
β : Type v
γ : Type ?u.32917
δ : Type ?u.32920
ε : Type ?u.32923
ζ : Type ?u.32926
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ 𝓝 (a, b) = Filter.prod (𝓝 a) (𝓝 b)
α : Type u
β : Type v
γ : Type ?u.32917
δ : Type ?u.32920
ε : Type ?u.32923
ζ : Type ?u.32926
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ 𝓝 (a, b) = 𝓝 a ×ˢ 𝓝 b
dsimp only [SProd.sprod]
no goals
α : Type u
β : Type v
γ : Type ?u.32917
δ : Type ?u.32920
ε : Type ?u.32923
ζ : Type ?u.32926
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ 𝓝 (a, b) = Filter.prod (𝓝 a) (𝓝 b)
rw [Filter.prod, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
  (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]