# Brouwer's fixed point theorem for infinite dimensional real space in subsystems of second order arithmetic

$\text{WKL}_0$ proves Brouwer's fixed point theorem for continuous functions on $\lbrack 0,1 \rbrack^n$, when $n$ is finite. What subsystem of second order arithmetic is needed to prove Brouwer's fixed point theorem for $\lbrack 0,1 \rbrack^\omega$ (i.e., the infinite dimensional unit interval)?

The following is provable in $\mathsf{WKL_0}$. Let $C$ be a nonempty closed convex set in $[−1, 1]^{\mathbb{N}}$ . Then every continuous function $f\colon C \to C$ has a fixed point.