Mathlib v3 is deprecated. Go to Mathlib v4

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

Modified src/topology/basic.lean

added theorem acc_iff_cluster

added theorem acc_principal_iff_cluster

added theorem acc_pt.mono

added def acc_pt

added theorem acc_pt_iff_frequently

added theorem acc_pt_iff_nhds

added theorem frequently_frequently_nhds

Created src/topology/perfect.lean

added theorem acc_pt.nhds_inter

added theorem exists_countable_union_perfect_of_is_closed

added theorem exists_perfect_nonempty_of_is_closed_of_not_countable

added theorem perfect.closure_nhds_inter

added theorem perfect.splitting

added structure perfect

added theorem preperfect.open_inter

added theorem preperfect.perfect_closure

added def preperfect

added theorem preperfect_iff_nhds

added theorem preperfect_iff_perfect_closure