English
The derived set derivedSet(A) consists of all accumulation points of A, i.e., points x such that every neighborhood of x intersects A in a point other than x (if x ∈ A) or in A at all (if x ∉ A).
Русский
Производное множество derivedSet(A) состоит из всех точек накопления множества A: каждая окрестность точки перечеркивает A в точке отличной от самой точки (или в A, если точка не принадлежит A).
LaTeX
$$$$\operatorname{derivedSet}(A) = \{x \mid \AccPt x (\mathcal{P} A)\}.$$$
Lean4
/-- The derived set of a set is the set of all accumulation points of it.
-/
def derivedSet (A : Set X) : Set X :=
{x | AccPt x (𝓟 A)}
