The image of a C¹ map between 3-manifolds is a neighbourhood of the image of an interior point where the derivative is injective

Let $M$ and $N$ be smooth 3-manifolds with boundary (modelled on the closed half-space), let $i:M\to N$ be a C¹ map, and let $x\in M$ be an interior point of $M$ at which the derivative $Di_x$ is injective. Then the image $i(M)$ is a neighbourhood of $i(x)$ in $N$:

In words: if a C¹ map between 3-manifolds has an invertible derivative at an interior point, then its image contains a neighbourhood of the image of that point. This is the inverse function theorem read in charts. A general fact, not stated in the paper; it is one of the facts behind footnote 2 of Section 1 (p. 2 of arXiv v1: the differentiable structure on W is compatible with those of U and V by restriction) and behind the fourth and fifth sentences of the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14), which state without proof that Λ_Z contains Λ_X and Λ_Y (through the inclusions) and use, without comment, that Λ_X and Λ_Y are hyperbolic sets of Z. In the proof of the companion statement plugGluing_local_conjugacy it shows that $i_U(U)$ is a neighbourhood of $i_U(x)$ for $x$ in the maximal invariant set $\Lambda_X$, which lies in the interior of $U$.

Formalization Note No embedding, injectivity, Hausdorff or compactness hypothesis is assumed; $i$ is only C¹ with $Di_x$ injective (hence a linear isomorphism of $\mathbb R^3$) at the one point $x$. Mathlib (at the pinned version) has no inverse function theorem on manifolds, so the proof goes through the chart representative and Mathlib's HasStrictFDerivAt.map_nhds_eq_of_equiv.