Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Quinn, thank you for the reference. They stress the non-constructiveness in great style: "Brouwer is known as one of the founders of intuitionism, which is one of the well-studied varieties of constructive mathematics and ironically, the theorem that he is best known for does not admit any constructive proof."
Will, I also can't see how to avoid some sort of approximation using such a scheme as you suggest. I even thought about intersecting the disk with a cubical grid, evaluating at the vertices, and refining dyadically, but of course as you said: I will still miss fixed points no matter what.
Dear Johannes, thank you for the answer. I am aware of the Sperner lemma, but was under the impression that using it would require me to triangulate the domain and simplicially approximate my function, which appears computationally intractable.
+1, I was going to mention CJS but of course Dai beat me to it. It is important to note that that this work was never published and so the results (particularly the hard part about Morse-Smale $f$ implying homeomorphism between $M$ and the classifying space of $C(f)$) should be carefully checked before being used.
We have to be careful with the simple homotopy claim. Given $f:X \to \mathbb{R}$ and setting $X^a = \lbrace \sigma \in X~|~f(\sigma) < a\rbrace $ there is a simple homotopy equivalence between $X^a$ and $X^b$ provided there are no critical values in $(a,b)$. On the other hand, when we cross a critical value, then we only have homotopy equivalence coming from the attaching map of the boundary of the critical cell: this need not be a simple homotopy equivalence.