A continuous self-map of a closed ball fixing its boundary sphere is onto the ball

Proved

Plasticity.Topology.closedBall_subset_image_of_eqOn_sphere

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

Let $V$ be a finite-dimensional real normed space, and let $g$ be continuous on the closed unit ball $B$ of $V$ with $g(z)=z$ for every unit vector $z$ . Then $B\subseteq g(B)$ .

Preamble

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

Formal statement

namespace Plasticity.Topology
theorem closedBall_subset_image_of_eqOn_sphere {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
    (g : V → V) (hg : ContinuousOn g (Metric.closedBall (0 : V) 1))
    (hid : ∀ z ∈ Metric.sphere (0 : V) 1, g z = z) :
    Metric.closedBall (0 : V) 1 ⊆ g '' Metric.closedBall (0 : V) 1 := by sorry
end Plasticity.Topology

Source

Classical consequence of the no-retraction theorem (card Plasticity.Ext.NoRetraction): a missed point would give a retraction of B onto its sphere

View graph