Nonexpansive bijections between balls of spaces between $c_{00}$ and $c_0$ are signed coordinate bijections

Proved

Plasticity.CUB37

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

Let $\Gamma,\Delta$ be sets, $X$ a space between $c_{00}(\Gamma)$ and $c_0(\Gamma)$ and $Y$ a space between $c_{00}(\Delta)$ and $c_0(\Delta)$ , both with the supremum norm, and let $F\colon B_X\to B_Y$ be a nonexpansive bijection of their closed unit balls. Suppose that $X=c_{00}(\Gamma)$ , or that $Y$ realizes all sign patterns (for instance $Y=c_0(\Delta)$ ). Then there are a bijection $\sigma\colon\Gamma\to\Delta$ and signs $\alpha_n\in\{1,-1\}$ such that

F(x)_{\sigma(n)}=\alpha_n x_n\qquad\text{for all }x\in B_X,\ n\in\Gamma;

that is, $F$ is the restriction of a signed coordinate bijection. No continuity of $F^{-1}$ is assumed.

Preamble

import Definitions.Def_Plasticity_SeqSpace
import Mathlib.Topology.EMetricSpace.Lipschitz

Formal statement

namespace Plasticity
theorem CUB37 {Γ Δ : Type*} (X : Submodule ℝ (Linf Γ)) (Y : Submodule ℝ (Linf Δ))
    (hX0 : c00 Γ ≤ X) (hX1 : X ≤ c0 Γ) (hY0 : c00 Δ ≤ Y) (hY1 : Y ≤ c0 Δ)
    (hmatch : X = c00 Γ ∨ RealizesSignPatterns Y)
    (F : Linf Γ → Linf Δ)
    (hbij : Set.BijOn F (ballIn X) (ballIn Y))
    (hlip : LipschitzOnWith 1 F (ballIn X)) :
    ∃ σ : Γ ≃ Δ, ∃ α : Γ → ℝ, (∀ n, α n = 1 ∨ α n = -1) ∧
      ∀ x ∈ ballIn X, ∀ n, F x (σ n) = α n * x n := by sorry
end Plasticity

Source

This repository: claim CUB37 (claims/cub.md), item (iii), in the form of Corollary 4 (i)–(ii) of expositions/c0_between_spaces.md; proof in §§2–4 there

Read-back

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

Setting. $\Gamma$ and $\Delta$ are arbitrary index types (possibly empty, finite, countably infinite or uncountable, and not assumed related to each other). $\ell_\infty(\Gamma)$ is the real Banach space of bounded functions $\Gamma \to \mathbb{R}$ with $\|x\|_\infty = \sup_\gamma |x(\gamma)|$ (and $\|x\|_\infty = 0$ when $\Gamma$ is empty); likewise $\ell_\infty(\Delta)$ . Recall

$c_{00}(\Gamma)$ : the finitely supported functions $\Gamma \to \mathbb{R}$ ;
$c_0(\Gamma)$ : the functions $x : \Gamma \to \mathbb{R}$ such that $\{\gamma : |x(\gamma)| \ge \varepsilon\}$ is finite for every $\varepsilon > 0$ ;

both regarded as linear subspaces of $\ell_\infty(\Gamma)$ , and similarly for $\Delta$ . The data are:

$X$ : a real linear subspace of $\ell_\infty(\Gamma)$ with $c_{00}(\Gamma) \subseteq X \subseteq c_0(\Gamma)$ ;
$Y$ : a real linear subspace of $\ell_\infty(\Delta)$ with $c_{00}(\Delta) \subseteq Y \subseteq c_0(\Delta)$ .

$X$ and $Y$ need not be closed or complete. Their closed unit balls, taken as subsets of the ambient $\ell_\infty$ spaces, are

B_X = \{x \in X : \|x\|_\infty \le 1\} \subseteq \ell_\infty(\Gamma), \qquad B_Y = \{y \in Y : \|y\|_\infty \le 1\} \subseteq \ell_\infty(\Delta).

$F : \ell_\infty(\Gamma) \to \ell_\infty(\Delta)$ is an arbitrary function on the whole of $\ell_\infty(\Gamma)$ ; only its values on $B_X$ matter. For $x \in \ell_\infty(\Gamma)$ and $\delta \in \Delta$ , $F(x)(\delta)$ denotes the $\delta$ -th coordinate of $F(x)$ .

Hypotheses.

(Matching condition) Either $X = c_{00}(\Gamma)$ exactly, or $Y$ realizes sign patterns, meaning: for every countable (finite, possibly empty, or countably infinite) set $C \subseteq \Delta$ and every $\varepsilon : \Delta \to \mathbb{R}$ with $\varepsilon(d) \in \{1, -1\}$ for all $d \in C$ , there is $v \in Y$ (no norm bound) with $\varepsilon(d)\, v(d) > 0$ for all $d \in C$ . The first alternative constrains only $X$ , the second only $Y$ .
(Bijection of balls) $F$ maps $B_X$ into $B_Y$ , $F$ is injective on $B_X$ , and every $y \in B_Y$ equals $F(x)$ for some $x \in B_X$ . Thus $F$ restricts to a bijection $B_X \to B_Y$ .
(Nonexpansive) $\|F(x) - F(x')\|_\infty \le \|x - x'\|_\infty$ for all $x, x' \in B_X$ .

Nothing is assumed about the inverse of $F|_{B_X}$ (no continuity or Lipschitz bound).

Conclusion. There exist a bijection $\sigma : \Gamma \to \Delta$ and signs $\alpha : \Gamma \to \mathbb{R}$ with $\alpha(n) = 1$ or $\alpha(n) = -1$ for every $n \in \Gamma$ , such that

F(x)(\sigma(n)) = \alpha(n)\, x(n) \qquad \text{for every } x \in B_X \text{ and every } n \in \Gamma.

Since $\sigma$ is a bijection, this fixes every coordinate of $F(x)$ : for $x \in B_X$ and $\delta \in \Delta$ , $F(x)(\delta) = \alpha(\sigma^{-1}\delta)\, x(\sigma^{-1}\delta)$ ; i.e. on $B_X$ , $F$ coincides with a signed coordinate permutation. In particular the conclusion asserts that $\Gamma$ and $\Delta$ are in bijection. Nothing is asserted about $F$ outside $B_X$ , and no statement relating $X$ and $Y$ beyond this formula is made explicitly.

Edge and satisfiability remarks.

The hypotheses are jointly satisfiable, e.g. by $\Gamma = \Delta$ , $X = Y = c_0(\Gamma)$ , $F$ the identity.
If $\Gamma$ is empty, then $B_X = \{0\}$ and hypothesis 2 forces $B_Y$ to be a single point; since $c_{00}(\Delta) \subseteq Y$ , this happens only if $\Delta$ is empty, and then the conclusion holds with the empty bijection. Symmetrically, $\Delta$ empty and $\Gamma$ nonempty is incompatible with injectivity in hypothesis 2.
If $\Delta$ is finite, then $Y = \ell_\infty(\Delta) = \mathbb{R}^\Delta$ and the second alternative of hypothesis 1 holds automatically. If $\Delta$ is infinite and $Y = c_{00}(\Delta)$ , the second alternative fails (a countably infinite $C$ would need $v$ with infinite support), so hypothesis 1 then requires $X = c_{00}(\Gamma)$ . If $Y = c_0(\Delta)$ , the second alternative holds, so $X$ may be any subspace between $c_{00}(\Gamma)$ and $c_0(\Gamma)$ .

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

Nonexpansive bijections between balls of spaces between c00c_{00}c00​ and c0c_0c0​ are signed coordinate bijections

Nonexpansive bijections between balls of spaces between $c_{00}$ and $c_0$ are signed coordinate bijections