Theorem: Invariance of domain

[SnirBroshi]

Wikipedia, Zulip 1 2

import Mathlib

-- useful notation from `PoincareConjecture.lean`
local macro:max "ℝ" noWs n:superscript(term) : term => `(EuclideanSpace ℝ (Fin $(⟨n.raw[0]⟩)))

theorem invariance_of_domain {n : ℕ} (U : Set ℝⁿ) (hU : IsOpen U) (f : C(U, ℝⁿ))
    (hf : f.toFun.Injective) : IsOpenMap f := by
  sorry

-- A cool corollary (described in the Wikipedia page):
theorem Real.homeomorph_eq {m n : ℕ} (f : ℝᵐ ≃ₜ ℝⁿ) : m = n := by
  sorry

Note that this theorem does not appear on the 100 theorems list nor on the 1000 theorems list.