The unit ball of $c_{00}(\Gamma)$ is plastic

The statement quantifies over every type $\Gamma$, in an arbitrary universe and of any cardinality. $\Gamma$ may be empty, finite, countably infinite or uncountable. The proof body is a placeholder, so the file only asserts the statement and proves nothing. The objects involved are as follows.

• $\ell_\infty(\Gamma)$. This is the set of functions $x:\Gamma\to\mathbb{R}$ for which $\{|x_i| : i\in\Gamma\}$ is bounded above. It has pointwise linear operations and the norm $\|x\|_\infty=\sup_{i\in\Gamma}|x_i|$, which is $0$ when $\Gamma$ is empty.
• $c_{00}(\Gamma)$. This is the real linear subspace of $\ell_\infty(\Gamma)$ consisting of the $x$ whose support $\{i\in\Gamma: x_i\neq 0\}$ is a finite set. Every finitely supported function is bounded, so $c_{00}(\Gamma)$ is exactly the set of all finitely supported functions $\Gamma\to\mathbb{R}$. It is treated as a real normed space in its own right, with the norm $\|\cdot\|_\infty$ restricted from $\ell_\infty(\Gamma)$.
• The ball $B$. This is the closed unit ball of that normed space:

Assertion. For every type $\Gamma$ and every map $f:B\to B$,

Here $f$ is an arbitrary bijection of $B$ onto itself. The statement assumes nothing about $f^{-1}$, does not require $f$ to be linear, and does not require $f(0)=0$. "Nonexpansive" means Lipschitz constant $1$ with the non-strict inequality $\le$.

Points to note:

• $\Gamma$ empty. $\ell_\infty(\Gamma)=c_{00}(\Gamma)=\{0\}$, so $B$ is a single point and the assertion is trivially true.
• $\Gamma$ finite with $n$ elements. $c_{00}(\Gamma)$ is all of $\mathbb{R}^\Gamma$ with the max norm, and $B$ is the cube $[-1,1]^n$ with the max metric. This is a compact metric space, a case covered by the classical fact that compact metric spaces are plastic. For finite $\Gamma$ this statement coincides with Thm_Plasticity_CUB36.
• No completeness. For infinite $\Gamma$ the space $c_{00}(\Gamma)$ with the sup norm is not complete. The statement concerns the ball of this incomplete space itself, not the ball of its completion.
• Unused imports. The imported definitions file also defines a set "ballIn", which is the same ball written as a subset of $\ell_\infty(\Gamma)$, and a property "RealizesSignPatterns". This statement uses neither. It takes the closed ball of the subspace regarded as a normed space, which carries the same sup metric.
• Real scalars only. The space is over $\mathbb{R}$ with the sup norm.