`closure_limit_point` can also be expressed as a disjoint union

[affeldt-aist]

analysis/theories/topology_theory/topology_structure.v

Line 690 in c9c9435

Lemma closure_limit_point E : closure E = E `|` limit_point E.

by introducing explicitly the notion of isolated point

@IshiguroYoshihiro