feat(topology): add basics of perfect sets (#17492)
add a file perfect.lean which contains basic definitions and facts about perfect sets as well as a version of the Cantor-Bendixson theorem. This is intended to build up to a proof of the Borel isomorphism theorem.
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>
Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
