Isolated point

Stream: Is there code for X?

[Andrew Yang]

What is the correct way to spell an isolated point?
Do we have the lemma below?

import topology.basic

lemma is_isolated_point_iff {α : Type*} [topological_space α] {x : α} :
  𝓝[≠] x = ⊥ ↔ is_open ({x} : set α) :=
by rw [← is_closed_compl_iff, ← closure_subset_iff_is_closed, set.subset_compl_singleton_iff,
    mem_closure_iff_nhds_within_ne_bot, filter.not_ne_bot]

[Reid Barton]

docs#not_is_open_singleton looks like the closest match