Rigidity: an inward nonexpansive bijection whose finitely supported images come from matched points is the identity

Proved

Plasticity.CUB37.rigidity

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

Let $X$ , $X'$ and $H\colon B_X\to B_{X'}$ be as in the no-collapse lemma: spaces between $c_{00}(\Gamma)$ and $c_0(\Gamma)$ , and a nonexpansive bijection moving every coordinate inward. Suppose that every $x\in B_X$ whose image $H(x)$ is finitely supported is matched in $X'$ . Then $H(x)=x$ for every $x\in B_X$ .

The finite cubes are then invariant under $H$ , Freudenthal–Hurewicz makes $H$ an isometry on each of them, and the inward property forces the identity on the dense set of finitely supported points.

Preamble

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

Formal statement

namespace Plasticity.CUB37
theorem rigidity {Γ : Type*} (X X' : Submodule ℝ (Linf Γ))
    (hX0 : c00 Γ ≤ X) (hX1 : X ≤ c0 Γ) (hX'0 : c00 Γ ≤ X') (hX'1 : X' ≤ c0 Γ)
    (H : Linf Γ → Linf Γ)
    (hbij : Set.BijOn H (ballIn X) (ballIn X'))
    (hlip : LipschitzOnWith 1 H (ballIn X))
    (hN1 : ∀ x ∈ ballIn X, ∀ n, (0 ≤ x n → 0 ≤ H x n ∧ H x n ≤ x n) ∧
      (x n ≤ 0 → x n ≤ H x n ∧ H x n ≤ 0))
    (hmatched : ∀ x ∈ ballIn X, (Function.support (H x)).Finite →
      ∃ w ∈ X', ∀ i, x i ≠ 0 → 0 < w i * x i) :
    ∀ x ∈ ballIn X, H x = x := by sorry
end Plasticity.CUB37

Source

This repository: expositions/c0_between_spaces.md §4, Theorem 3

View graph