Invariance of domain

Fix $x\in U$. Openness gives $\rho >0$ with $B(x,\rho )\subset U$; take the closed ball $D=\bar{B}(x,\rho \mathrm{/}2)$. It is compact by [F5]. The restriction $f{\mathrm{\mid }}_D$ is a homeomorphism onto its image: it is a continuous bijection there by injectivity, and it sends every closed $F\subset D$ to a closed subset of $f(D)$. Indeed $F$ is closed and bounded in Euclidean space, hence compact by [F5]; a cover of $f(F)$ pulls back to a cover of $F$, proving compactness of the image; and [F2] makes that image closed. Thus the inverse has closed preimages of closed sets and is continuous. The same reasoning applies to the boundary $\mathrm{\partial }D\cong S^{n-1}$. View both images in $S^n$ using the chart of [F3].

The compact subset $f(D)$ is proper in $S^n$ since it avoids $\mathrm{\infty }$, is nonempty, and is weakly locally contractible by the homeomorphism in step 1.1. In the ball $D$, intersection with any sufficiently small ball about one of its points is convex, so contracts within any prescribed relative neighborhood after making the radius small; this includes boundary points. Also $D$ contracts to its center by the straight-line homotopy. Its reduced integral cohomology is zero in every degree by [F6]: for a point, the unnormalized cochain groups are $\mathbb{Z}$ in every nonnegative degree and their coboundaries alternate zero and identity, giving only the constant class in degree zero. Consequently [F3] gives ${\tilde{H}}_0(S^n\setminus f(D);\mathbb{Z})=0$. The complement contains $\mathrm{\infty }$, so [F4] proves that it is path connected. This supplies the connectedness of the disk complement without an implicit separation theorem.

The spherical statement [F1] applied to $f(\mathrm{\partial }D)$ gives exactly two path components of $S^n\setminus f(\mathrm{\partial }D)$. This complement is open by compactness and [F2]. Its path components are open: about each point choose a path-connected coordinate ball lying in this open complement; it is contained in that point's path component, so the component is a union of such open balls.

There is a disjoint union of sets $S^n\setminus f(\mathrm{\partial }D)=f(\mathrm{int}D)\bigsqcup (S^n\setminus f(D))\mathrm{.}$ Injectivity gives the equality $f(D)\setminus f(\mathrm{\partial }D)=f(\mathrm{int}D)$. Both displayed sets are nonempty and path connected: the first is the continuous image of the convex open ball and contains $f(x)$; the second has this property by step 2.1. Each therefore lies in a single path component of the boundary complement. Since together they exhaust a space having exactly two path components by step 2.2, they must lie in distinct components and equal those components; otherwise the other component would have no point in their union. Hence $f(\mathrm{int}D)$ is open in $S^n$ by step 2.2, and therefore open in its chart ${\mathbb{R}}^n$. It is an open neighborhood of $f(x)$ contained in $f(U)$.

Each point of $f(U)$ has such an open neighborhood by step 3.1, so their union $f(U)$ is open; this statement requires no simultaneous selection of balls. If $V$ is any open subset of $U$, it is open in ${\mathbb{R}}^n$ since $U$ is open, and $f{\mathrm{\mid }}_V$ has the same continuity and injectivity hypotheses. Applying steps 1.1–3.1 to each point of $V$ gives that $f(V)$ is open in ${\mathbb{R}}^n$. Thus the bijection $f:U\to f(U)$ is open. Its inverse is continuous because the inverse image under $f^{-1}$ of any open $V\subset U$ is exactly $f(V)$, open in $f(U)$. This proves the homeomorphism conclusion.

The dimension-zero and empty cases were treated in the Given paragraph. In dimension one the proof uses the valid two-component statement in $S^1$ for the two-point boundary, not the false two-component assertion for that boundary in $\mathbb{R}$. Both the source ball and its image are allowed to have boundaries, but no assumption that the original map is already open or has continuous inverse was made. All coefficient calculations use integral groups solely to detect components, and do not rely on a nondegenerate singular-chain model. The AC use is exactly [F7]'s inherited duality assumption; compact image arguments, the choice of one ball at a fixed point, and taking the union of all resulting image neighborhoods add no AC.