A few results about the Cantor set

Stream: mathlib4

[Francesco Vercellesi]

Hello,
I recently had to formalise a few results about the Cantor set which I could not find on Mathlib and I would now like to contribute them.
The results are:

• The cardinality of the cantor set
• The fact that the cantor set has empty interior

My fork is at https://github.com/franv314/mathlib4, and I'd like to clean it up a bit before actually opening a PR.
Please feel free to suggest changes

[Kenny Lau]

we currently have exactly 8 facts about the cantor set so I think any more lemmas would be welcome

[Kenny Lau]

@loogle cantorSet

[loogle]

:search: cantorSet, isClosed_cantorSet, and 6 more

[Kenny Lau]

also, it's easier to suggest stuff after you make the PR

[Kenny Lau]

one comment I will make, is that right now it seems like your code is specifically about the cantor set, when I'm sure a lot of the arguments can be generalised to two numbers that are not 1/3 and 2/3, or even more than two numbers

[Francesco Vercellesi]

I've opened #30229

[Aaron Liu]

Do we have properties of the abstract cantor set Nat -> Bool?

[Aaron Liu]

Does any docs#Topology.IsEmbedding (Nat -> Bool) -> Real also have nowhere dense range?

[Aaron Liu]

Can this be generalized away from Real?

[Aaron Liu]

I see docs#Cardinal.cantorFunction

[Sébastien Gouëzel]

You're talking about the Cantor set here, but I'm not sure what you mean. For me, a Cantor set is a compact second countable totally disconnected space without isolated points, of which your Cantor set is just one very special instance. Do we have the theorem that all these are homeomorphic, for instance?

[Aaron Liu]

I feel like Nat -> Bool is a "standard" cantor set and other cantor sets like Nat -> ENat are not mentioned as often

[Aaron Liu]

The other standard cantor set is the middle-thirds set (or rather, the without middle-thirds set) which is a subset of Icc (0 : Real) 1

[Francesco Vercellesi]

My goal was really only to expand on the currently defined cantor set (which is the middle-thirds set).
I'm unaware of any results about the abstract cantor set Nat -> Bool in mathlib4 but I agree that it would make sense to prove that these are homeomorphic instead of that they just have the same cardinality

[Alex Meiburg]

It would be excellent if we could find a workable definition general enough to encompass https://en.wikipedia.org/wiki/Smith%E2%80%93Volterra%E2%80%93Cantor_set as well. (Which was chronologically prior!)