Recent searches
Search options
Are there space-filling curves, constructively? A blog post with pictures and animations. https://math.andrej.com/2024/01/30/space-filling-curves-constructively/
@andrejbauer
Two questions
* Which spaces admit a space filling curve? Classically, it suffices that they be compact, locally connected, separable. But in general?
* I'm not fluent enough in topos theory: if the square is not covered by a curve in the sheaf topos, that means (does it?) that there are points of this topos which are missed by any given curve. Can one explicit such points?
@andrejbauer I wonder if Murray Polygons would help...
https://info.cs.st-andrews.ac.uk/student-handbook/school/jack-cole/murray-polygon.html
Code (S-Algol) is available:
https://info.cs.st-andrews.ac.uk/student-handbook/school/jack-cole/murray-polygon-code.html
@andrejbauer I love seeing the hilbert curve in action. I remember using it ages ago as a strategy for Tower Defense games
@andrejbauer The danger of reading mathstodon is that it tends to expand my todo list (in this case, https://github.com/metamath/set.mm/issues/3812 which just says to formalize that blog post). But this is a good thing and it isn't really "my" todo list in that it is equally aimed at anyone who formalizes in Metamath or wants to start.
@andrejbauer Image description: three curves each of which add to the previous one by replacing line segments with more folded curves. The limit of this process will be a space filling curve.
@andrejbauer you can prove theorem 2 without choice for the Cauchy reals. Thus, countable choice implies it for the Dedekind reals.