Return to Answer

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this:

Theorem (constructive Brouwer fixed-point theorem)

Let $B$ be the closed unit ball in $\mathbb{R}^n$ for $n\in\mathbb{N}$, and let $f$ be a uniformly continuous function from $B$ to itself. Let $G_f=\{(x,f(x))|\,x\in B\}$ be the graph of $f$ in $B\times B$, and let $D$ be the diagonal $\{(x,x)|\,x\in B\}$, also in $B\times B$.

Then $d(G_f, D)=0$.

This version is short, and yet provides all the constructive information needed for approximative BFP-versions.

[update for clarification, oct 2019:]

• For two subsets $A, B$ and $\rho\geq 0$ we write $d(A, B)=\rho$ when we can determine that $\inf(\{d(a,b)| a\in A, b\in B\})$ exists constructively and equals $\rho$.
• The above phrasing of the theorem is classically equivalent to the usual phrasing of the BFPT.

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this:

Theorem (constructive Brouwer fixed-point theorem)

Let $B$ be the closed unit ball in $\mathbb{R}^n$ for $n\in\mathbb{N}$, and let $f$ be a uniformly continuous function from $B$ to itself. Let $G_f=\{(x,f(x))|\,x\in B\}$ be the graph of $f$ in $B\times B$, and let $D$ be the diagonal $\{(x,x)|\,x\in B\}$, also in $B\times B$.

Then $d(G_f, D)=0$.

This version is short, and yet provides all the constructive information needed for approximative BFP-versions.

[update for clarification, oct 2019:]

• For two subsets $A, B$ and $\rho\geq 0$ we write $d(A, B)=\rho$ when we can determine that $\inf(\{d(a,b)| a\in A, b\in B\})$ exists constructively and equals $\rho$.
• The above phrasing of the theorem is classically equivalent to the usual phrasing of the BFPT. (That also holds for Simon Henry's answer which in essence gives the same theorem. Still, one doesn't need a localic approach to prove it, it holds in plain BISH).

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this:

Theorem (constructive Brouwer fixed-point theorem)

Let $B$ be the closed unit ball in $\mathbb{R}^n$ for $n\in\mathbb{N}$, and let $f$ be a uniformly continuous function from $B$ to itself. Let $G_f=\{(x,f(x))|\,x\in B\}$ be the graph of $f$ in $B\times B$, and let $D$ be the diagonal $\{(x,x)|\,x\in B\}$, also in $B\times B$.

Then $d(G_f, D)=0$.

This version is short, and yet provides all the constructive information needed for approximative BFP-versions.

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this:

Theorem (constructive Brouwer fixed-point theorem)

Let $B$ be the closed unit ball in $\mathbb{R}^n$ for $n\in\mathbb{N}$, and let $f$ be a uniformly continuous function from $B$ to itself. Let $G_f=\{(x,f(x))|\,x\in B\}$ be the graph of $f$ in $B\times B$, and let $D$ be the diagonal $\{(x,x)|\,x\in B\}$, also in $B\times B$.

Then $d(G_f, D)=0$.

This version is short, and yet provides all the constructive information needed for approximative BFP-versions.

[update for clarification, oct 2019:]

• For two subsets $A, B$ and $\rho\geq 0$ we write $d(A, B)=\rho$ when we can determine that $\inf(\{d(a,b)| a\in A, b\in B\})$ exists constructively and equals $\rho$.
• The above phrasing of the theorem is classically equivalent to the usual phrasing of the BFPT.

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this:

Theorem (constructive Brouwer fixed-point theorem)

Let $B$ be the unit ball in $\mathbb{R}^n$ for $n\in\mathbb{N}$, and let $f$ be a uniformly continuous function from $B$ to itself. Let $G_f=\{(x,f(x))|\,x\in B\}$ be the graph of $f$ in $B\times B$, and let $D$ be the diagonal $\{(x,x)|\,x\in B\}$, also in $B\times B$.

Then $d(G_f, D)=0$.

This version is short, and yet provides all the constructive information needed for approximative BFP-versions.

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this:

Theorem (constructive Brouwer fixed-point theorem)

Let $B$ be the closed unit ball in $\mathbb{R}^n$ for $n\in\mathbb{N}$, and let $f$ be a uniformly continuous function from $B$ to itself. Let $G_f=\{(x,f(x))|\,x\in B\}$ be the graph of $f$ in $B\times B$, and let $D$ be the diagonal $\{(x,x)|\,x\in B\}$, also in $B\times B$.

Then $d(G_f, D)=0$.

This version is short, and yet provides all the constructive information needed for approximative BFP-versions.