mathlib

49b7f94a - feat(topology/perfect): Schemes, embedding of the Cantor space (#18248)

feat(topology/perfect): Schemes, embedding of the Cantor space (#18248) Add to `topology.perfect` the following theorem: In a complete metric space, any nonempty perfect set admits a continuous embedding of the Cantor space. The proof uses an object which in descriptive set theory is sometimes called a "scheme". Some attempt was made to include in `topology.metric_space.cantor_scheme` a general theory of these schemes, since they should be useful down the line in other results as well. We also define `pi_nat.res` in `topology.metric_space.pi_nat`.