Commit 2022-12-18 16:44 138f1db8

View on Github →

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.

Estimated changes

added theorem acc_iff_cluster
added theorem acc_pt.mono
added def acc_pt
added theorem acc_pt_iff_frequently
added theorem acc_pt_iff_nhds