case a
α : Type u_1
β : Type ?u.11780
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
s✝ : Set α
⊢ s✝ ∈ 𝓝ˢ {x} ↔ s✝ ∈ 𝓝 x
α : Type u_1
β : Type ?u.11780
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ {x} = 𝓝 x
ext
no goals
case a
α : Type u_1
β : Type ?u.11780
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
s✝ : Set α
⊢ s✝ ∈ 𝓝ˢ {x} ↔ s✝ ∈ 𝓝 x
rw [← subset_interior_iff_mem_nhdsSet, ← mem_interior_iff_mem_nhds, singleton_subset_iff]