Sphere covered by finite-dimensional faces: every nonexpansive bijection onto the ball is linear

Proved

Plasticity.Faces.exists_linearIsometryEquiv_of_sphere_covered

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

Let $X,Y$ be real Banach spaces such that every point of the unit sphere of $Y$ lies in a finite-dimensional face of $B_Y$ contained in the sphere. Then every nonexpansive bijection $F\colon B_X\to B_Y$ is the restriction of a surjective linear isometry $T\colon X\to Y$ . This removes the polyhedrality hypothesis from Theorem 4.11 of Angosto, Kadets and Zavarzina, where the sphere is a union of finite-dimensional polyhedral extreme subsets.

Preamble

import Definitions.Def_Plasticity_Faces
import Mathlib.Analysis.Normed.Operator.LinearIsometry
import Mathlib.Topology.EMetricSpace.Lipschitz

Formal statement

namespace Plasticity.Faces
theorem exists_linearIsometryEquiv_of_sphere_covered {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]
    (F : X → Y)
    (hbij : Set.BijOn F (Metric.closedBall (0 : X) 1) (Metric.closedBall (0 : Y) 1))
    (hlip : LipschitzOnWith 1 F (Metric.closedBall (0 : X) 1))
    (hcover : ∀ y ∈ Metric.sphere (0 : Y) 1, ∃ C : Set Y,
      IsSphereFace C ∧ FiniteDimensional ℝ (vectorSpan ℝ C) ∧ y ∈ C) :
    ∃ T : X ≃ₗᵢ[ℝ] Y, Set.EqOn F T (Metric.closedBall (0 : X) 1) := by sorry
end Plasticity.Faces

Source

This repository: claim F17 (claims/f.md), Corollary 3 of expositions/faces/finite_faces_boundary_crossing.md, through §6 of expositions/faces/codirected_compactness.md (claim F11) and the sphere-preservation theorem U10; compare C. Angosto, V. Kadets, O. Zavarzina, J. Math. Anal. Appl. 471 (2019), Theorem 4.11

Read-back

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

Read-back. Assume the standing hypotheses ( $X, Y$ real Banach; $F$ maps $B_X$ injectively onto $B_Y$ ; $F$ is 1-Lipschitz on $B_X$ ). Assume that every $y \in S_Y$ lies in some sphere face $C$ of $B_Y$ (nonempty, convex, $C \subseteq S_Y$ , extreme subset of $B_Y$ ) whose span of $C - C$ is finite-dimensional. Then there is a bijective linear map $T : X \to Y$ with $\|Tx\| = \|x\|$ for all $x$ such that $F(x) = T(x)$ for every $x \in B_X$ . The covering hypothesis is on the target $Y$ only; $X$ is an arbitrary real Banach space.

Flags.

Conventions. Degenerate cases: if $Y = 0$ the hypothesis is vacuous and bijectivity forces $X = 0$ ; if $X = 0 \ne Y$ the hypotheses cannot hold. Both consistent.
Hypotheses. None unused or missing.
Name. Accurate; "sphere_covered" abbreviates "sphere covered by finite-dimensional sphere faces", and the agreement $F = T$ on $B_X$ is left implicit (minor).
Truth. Not refuted; not verified. It is equivalent to " $F$ is an isometry" (a surjective isometry between the balls extends to an affine isometry, and $F(0) = 0$ ). To my recollection, special cases are published: $Y$ strictly convex (all faces are points; Cascales, Kadets, Orihuela, Wingler) and spheres that are unions of finite-dimensional polyhedral extreme subsets (Angosto, Kadets, Zavarzina); finite-dimensional $Y$ also satisfies the hypothesis. The non-polyhedral infinite-dimensional case is beyond those, and I did not verify it.

Human review

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

View graph