A nonempty compact convex set with finite-dimensional span is a closed ball in its direction space

Proved

Plasticity.Topology.exists_closedBall_model_of_convex_compact

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

Let $C$ be a nonempty compact convex subset of a real normed space whose affine hull is finite-dimensional, with direction space $V=\operatorname{span}(C-C)$ . There are continuous maps $\varphi\colon V\to E$ and $\psi\colon E\to V$ such that $\varphi$ maps the closed unit ball of $V$ onto $C$ with inverse $\psi$ on $C$ , and $\varphi(z)$ lies in the relative boundary of $C$ exactly when $\|z\|=1$ .

Preamble

import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.Convex.Intrinsic

Formal statement

namespace Plasticity.Topology
theorem exists_closedBall_model_of_convex_compact {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : Set E)
    (hcpt : IsCompact C) (hconv : Convex ℝ C) (hne : C.Nonempty)
    (hfin : FiniteDimensional ℝ (vectorSpan ℝ C)) :
    ∃ φ : vectorSpan ℝ C → E, ∃ ψ : E → vectorSpan ℝ C, Continuous φ ∧ Continuous ψ ∧
      (∀ z : vectorSpan ℝ C, ‖z‖ ≤ 1 →
        φ z ∈ C ∧ ψ (φ z) = z ∧ (φ z ∈ intrinsicFrontier ℝ C ↔ ‖z‖ = 1)) ∧
      ∀ y ∈ C, ‖ψ y‖ ≤ 1 ∧ φ (ψ y) = y := by sorry
end Plasticity.Topology

Source

Radial projection from a relative-interior point; Mathlib's gauge rescaling (Mathlib/Analysis/Convex/GaugeRescale.lean)

View graph