Binary expansions of real numbers in `[0,1]`

Stream: Is there code for X?

[Markus de Medeiros]

Can't seem to figure out the right search terms for this though I've seen some people on here suggest it may exist. I'm searching for two functions expand : Icc 0 1 → (ℕ → Bool) and unexpand : (ℕ → Bool) → Icc 0 1 as well as the one inverse that is true expand ∘ unexpand = id

[Robin Arnez]

That was literally merged yesterday: #26021

[Markus de Medeiros]

Haha awesome!

[Markus de Medeiros]

Thanks!