α✝ : Type ?u.6536
β : Type ?u.6539
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α✝
x : α✝
α : Type u_1
inst✝ : TopologicalSpace (α × α)
⊢ sSup (range (𝓝 ∘ fun x => (x, x))) = ⨆ (x : α), 𝓝 (x, x)
α✝ : Type ?u.6536
β : Type ?u.6539
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α✝
x : α✝
α : Type u_1
inst✝ : TopologicalSpace (α × α)
⊢ 𝓝ˢ (diagonal α) = ⨆ (x : α), 𝓝 (x, x)
rw [nhdsSet, ← range_diag, ← range_comp]
no goals
α✝ : Type ?u.6536
β : Type ?u.6539
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α✝
x : α✝
α : Type u_1
inst✝ : TopologicalSpace (α × α)
⊢ sSup (range (𝓝 ∘ fun x => (x, x))) = ⨆ (x : α), 𝓝 (x, x)
rfl