α : Type u
β : Type v
γ : Type ?u.39611
δ : Type ?u.39614
ε : Type ?u.39617
ζ : Type ?u.39620
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ map (fun p => (p.snd, p.fst)) (𝓝 b ×ˢ 𝓝 a) = map Prod.swap (𝓝 b ×ˢ 𝓝 a)
α : Type u
β : Type v
γ : Type ?u.39611
δ : Type ?u.39614
ε : Type ?u.39617
ζ : Type ?u.39620
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ 𝓝 (a, b) = map Prod.swap (𝓝 (b, a))
rw [nhds_prod_eq, Filter.prod_comm, nhds_prod_eq]
no goals
α : Type u
β : Type v
γ : Type ?u.39611
δ : Type ?u.39614
ε : Type ?u.39617
ζ : Type ?u.39620
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ map (fun p => (p.snd, p.fst)) (𝓝 b ×ˢ 𝓝 a) = map Prod.swap (𝓝 b ×ˢ 𝓝 a)
rfl