The unit ball of $c_0(\Gamma)$ is plastic

Proved

Plasticity.CUB36

by scanstone · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

For every set $\Gamma$ , every nonexpansive bijection of the closed unit ball of $c_0(\Gamma)$ (real functions on $\Gamma$ vanishing at infinity, supremum norm) onto itself is an isometry. No continuity of the inverse is assumed.

Preamble

import Definitions.Def_Plasticity_Basic
import Definitions.Def_Plasticity_SeqSpace

Formal statement

namespace Plasticity
theorem CUB36 (Γ : Type*) : HasPlasticUnitBall (c0 Γ) := by sorry
end Plasticity

Source

This repository: claim CUB36 (claims/cub.md, for Γ = ℕ) and expositions/c0_between_spaces.md, Corollary 4 (iii), for every Γ

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

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_0(\Gamma)$ . This is the real linear subspace of $\ell_\infty(\Gamma)$ consisting of the $x$ with $x_i\to 0$ along the cofinite filter on $\Gamma$ . Equivalently,

\forall \varepsilon>0:\quad \{\,i\in\Gamma:\ |x_i|\ge\varepsilon\,\}\ \text{is finite}.

Such functions are automatically bounded, so $c_0(\Gamma)$ is exactly the set of real functions on $\Gamma$ that vanish at infinity. Each of them has countable support, even when $\Gamma$ is uncountable. $c_0(\Gamma)$ 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:

B=\{x\in c_0(\Gamma):\ \|x\|_\infty\le 1\},\qquad d(x,y)=\sup_{i\in\Gamma}|x_i-y_i|.

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

\Big(\forall x,y\in B:\ \|f(x)-f(y)\|_\infty\le\|x-y\|_\infty\Big)\ \wedge\ f\text{ is bijective} \ \Longrightarrow\ \forall x,y\in B:\ \|f(x)-f(y)\|_\infty=\|x-y\|_\infty .

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. $c_0(\Gamma)=\{0\}$ , so $B$ is a single point and the assertion is trivially true.
$\Gamma$ finite with $n$ elements. The cofinite filter on a finite set is the trivial (bottom) filter, so the convergence condition holds for every $x$ . Then $c_0(\Gamma)=\ell_\infty(\Gamma)=\mathbb{R}^\Gamma$ with the max norm, and $B$ is the compact cube $[-1,1]^n$ , a case covered by the classical fact that compact metric spaces are plastic. For finite $\Gamma$ this statement coincides with Thm_Plasticity_CUB35.
Completeness. For every $\Gamma$ , $c_0(\Gamma)$ is closed in $\ell_\infty(\Gamma)$ and so is complete. The statement nevertheless carries no completeness hypothesis of its own.
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.

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by scanstone · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The unit ball of c0(Γ)c_0(\Gamma)c0​(Γ) is plastic

The unit ball of $c_0(\Gamma)$ is plastic