Invariance of domain in $\mathbb R^\iota$

Proved

Plasticity.Ext.InvarianceOfDomain

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

Let $\iota$ be a finite set, $U\subseteq\mathbb R^\iota$ open, and $f\colon U\to\mathbb R^\iota$ continuous and injective. Then $f(U)$ is open.

It is used to show that a nonexpansive bijection of a ball between $c_{00}$ and $c_0$ cannot collapse a coordinate of a matched point.

Formalization Note $f$ is a function on all of $\mathbb R^\iota$ , constrained on $U$ by ContinuousOn and Set.InjOn.

Preamble

import Mathlib.Topology.Order.Basic
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Topology.ContinuousOn

Formal statement

namespace Plasticity.Ext
theorem InvarianceOfDomain {ι : Type*} [Fintype ι] (U : Set (ι → ℝ)) (hU : IsOpen U)
    (f : (ι → ℝ) → (ι → ℝ)) (hf : ContinuousOn f U) (hinj : Set.InjOn f U) :
    IsOpen (f '' U) := by sorry
end Plasticity.Ext

Source

L. E. J. Brouwer, Beweis der Invarianz des n-dimensionalen Gebietes, Math. Ann. 71 (1912), 305–313; proof from the Brouwer fixed-point theorem as in W. Kulpa, Poincaré and domain invariance theorem, Acta Univ. Carolin. Math. Phys. 39 (1998), 127–136

View graph

Invariance of domain in Rι\mathbb R^\iotaRι

Invariance of domain in $\mathbb R^\iota$