Invariance of dimension

Proved

Plasticity.Ext.InvarianceOfDimension

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

Let $V,W$ be finite-dimensional real normed spaces, $U\subseteq V$ a nonempty open set, and $f\colon U\to W$ continuous and injective. Then $\dim V\le\dim W$ .

Preamble

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

Formal statement

namespace Plasticity.Ext
theorem InvarianceOfDimension {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    (U : Set V) (hU : IsOpen U) (hne : U.Nonempty) (f : V → W)
    (hf : ContinuousOn f U) (hinj : Set.InjOn f U) :
    Module.finrank ℝ V ≤ Module.finrank ℝ W := by sorry
end Plasticity.Ext

Source

L. E. J. Brouwer, Beweis der Invarianz der Dimensionenzahl, Math. Ann. 70 (1911); here a consequence of invariance of domain (card Plasticity.Ext.InvarianceOfDomain)

View graph