Finite set has no accumulation points

Stream: Is there code for X?

[Nir Paz]

Do we have something close to the fact that in a T1 space a finite set has an empty derivedSet? The literal statement doesn't exist but maybe I'm missing something close.

[Yury G. Kudryashov]

I think, the closest facts we have are docs#infinite_of_mem_nhds and docs#Finite.instDiscreteTopology

[Nir Paz]

Actually I only need that the derivedSet is not larger than the set itself, which follows from docs#Set.Finite.isClosed and docs#isClosed_iff_derivedSet_subset.