α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hx : x ∈ s
this : {{ val := x, property := hx }} ∈ 𝓝 { val := x, property := hx }
⊢ {x} ∈ 𝓝[s] x
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hx : x ∈ s
⊢ {x} ∈ 𝓝[s] x
have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hx : x ∈ s
this : {{ val := x, property := hx }} ∈ 𝓝 { val := x, property := hx }
⊢ {x} ∈ 𝓝[s] x
simpa only [nhdsWithin_eq_map_subtype_coe hx, image_singleton] using
  @image_mem_map _ _ _ ((↑) : s → α) _ this
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hx : x ∈ s
⊢ {{ val := x, property := hx }} ∈ 𝓝 { val := x, property := hx }
simp [nhds_discrete]