Cantor set, Cantor function?

Stream: Is there code for X?

[Michael Rothgang]

Is there a definition of the (standard) Cantor set $C$ and the (Vitali-Lebesgue-)Cantor staircase function $f:[0,1]\to [0,1]$ --- or, aiming for the moon on a stick, even the following properties?

• $C$ is uncountable, nowhere dense and has measure zero
• $f$ is continuous
• $f([0,1]\setminus C)$ is countable, so $f(C)$ has measure $1$
• (I don't need this, but it's still cool: $f'(t)=0$ a.e., so $f(1)\neq \int_0^1 f'(t)dt$ and $f$ is not absolutely continuous)
• huge bonus points for fat Cantor sets -- showing that nowhere dense doesn't imply Lebesgue measure zero

Then I could also state a counterexample to a lemma I'm currently formalizing. :-)

[Kevin Buzzard]

I don't know the answer to your actual question but I would recommend that you stop formalising the lemma.

[Kevin Buzzard]

As to your question, certainly most if not all of it would be accessible (and perhaps even easy and fun) given what we already have.

[Michael Rothgang]

Kevin Buzzard said:

I don't know the answer to your actual question but I would recommend that you stop formalising the lemma.

I've been imprecise: I wasn't trying to formulate a false statement - rather, it's an example why a particular hypothesis (some function being C¹) cannot be weakened.