A convex set mapped continuously and injectively into a finite-dimensional affine subspace has no larger dimension

Proved

Plasticity.Topology.finrank_vectorSpan_le_of_injOn

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

Let $D$ be a convex subset of a real normed space, $W$ a finite-dimensional subspace of another, $c$ a point, and $f$ continuous and injective on $D$ with $f(x)-c\in W$ for $x\in D$ . Then the affine hull of $D$ is finite-dimensional and $\dim\operatorname{span}(D-D)\le\dim W$ .

Preamble

import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.Convex.Basic
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Formal statement

namespace Plasticity.Topology
theorem finrank_vectorSpan_le_of_injOn {E E' : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup E'] [NormedSpace ℝ E'] (D : Set E) (hconv : Convex ℝ D)
    (f : E → E') (hf : ContinuousOn f D) (hinj : Set.InjOn f D)
    (W : Submodule ℝ E') (hW : FiniteDimensional ℝ W) (c : E') (hc : ∀ x ∈ D, f x - c ∈ W) :
    FiniteDimensional ℝ (vectorSpan ℝ D) ∧
      Module.finrank ℝ (vectorSpan ℝ D) ≤ Module.finrank ℝ W := by sorry
end Plasticity.Topology

Source

Invariance of dimension (card Plasticity.Ext.InvarianceOfDimension)

View graph