No retraction of a closed ball onto its boundary sphere

Proved

Plasticity.Ext.NoRetraction

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

Let $V$ be a nonzero finite-dimensional real normed space with closed unit ball $B$ and unit sphere $S$ . If $r\colon B\to S$ is continuous, then $r(x)\ne x$ for some $x\in S$ : there is no continuous retraction of $B$ onto $S$ .

Preamble

import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Topology.ContinuousOn

Formal statement

namespace Plasticity.Ext
theorem NoRetraction {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
    [Nontrivial V] (r : V → V) (hr : ContinuousOn r (Metric.closedBall (0 : V) 1))
    (hmaps : Set.MapsTo r (Metric.closedBall (0 : V) 1) (Metric.sphere (0 : V) 1)) :
    ∃ x ∈ Metric.sphere (0 : V) 1, r x ≠ x := by sorry
end Plasticity.Ext

Source

Classical, equivalent to Brouwer's fixed-point theorem: if r were a retraction, −r would map the ball into the sphere without a fixed point (L. E. J. Brouwer, Über Abbildung von Mannigfaltigkeiten, Math. Ann. 71 (1912))

View graph