I think the relevant topology on the space of binary streams is the Cantor space.[0] It's compact, and can be seen as a subspace of the real line.[1] The fact t

I think the relevant topology on the space of binary streams is the Cantor space.[0] It's compact, and can be seen as a subspace of the real line.[1] The fact that it's compact is equivalent to a principle called the fan theorem, which is simply true in classical mathematics, but which different schools of constructive mathematics don't agree on.[2] [0]: https://ncatlab.org/nlab/show/Cantor+space https://ncatlab.org/nlab/show/Cantor+space [1]: https://en.wikipedia.org/wiki/Cantor_set https://en.wikipedia.org/wiki/Cantor_set [2]: https://ncatlab.org/nlab/show/fan+theorem https://ncatlab.org/nlab/show/fan+theorem