Invariance of domain between finite-dimensional normed spaces of equal dimension

Proved

Plasticity.Topology.isOpen_image_of_injOn_of_finrank_eq

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

Let $V,W$ be finite-dimensional real normed spaces of the same dimension, $U\subseteq V$ open, and $f$ continuous and injective on $U$ . Then $f(U)$ is open in $W$ .

Preamble

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

Formal statement

namespace Plasticity.Topology
theorem isOpen_image_of_injOn_of_finrank_eq {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    (hdim : Module.finrank ℝ V = Module.finrank ℝ W)
    (U : Set V) (hU : IsOpen U) (f : V → W) (hf : ContinuousOn f U) (hinj : Set.InjOn f U) :
    IsOpen (f '' U) := by sorry
end Plasticity.Topology

Source

L. E. J. Brouwer, Beweis der Invarianz des n-dimensionalen Gebiets, Math. Ann. 71 (1912); from the card Plasticity.Ext.InvarianceOfDomain

View graph