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

Question

$\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)?

Answer 1

Too long for a comment (and if I'm missing a subtlety, my apologies):

Stephen Simpson's Subsystems of Second Order Arithmetic, second edition, Theorem IV.7.9, page 152, proves Schauder's fixed point theorem which seems to be what you're looking for:

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.

The entire section IV.7 is devoted to fixed point theorems.