Should Preperfect be renamed to DenseInItself?

Stream: mathlib4

[Daniel Weber]

According to the implementation notes in Mathlib.Topology.Perfect:

We define a nonstandard predicate, Preperfect, which drops the closed-ness requirement from the definition of perfect.

But every point in a set being an accumulation point of it is exactly the condition for a set to be dense-in-itself.

[Antoine Chambert-Loir]

I do not recommend the terminology “Dense in itself” which is ambiguous (because every set is dense in itself). Wikipedia suggests Crowded, but since we have NoZeroDivisors, I feel that NoIsolatedPoints would be even better.