Tubular neighbourhoods with a variable radius

Every C² embedded boundaryless manifold in a finite-dimensional real inner product space has a tubular neighbourhood with a positive continuous radius. Compactness and closedness of the embedded image are not required. The addition map on the normal bundle is an open embedding on this neighbourhood.

The local normal-map theorem is exists_injOn_isOpen_image_normalTube. The continuous radius is chosen so that any two intersecting normal discs have their base points in one local injectivity neighbourhood: use the larger of their two radii. This avoids the uniform separation bound available only for a compact core.

The result concerns the topology of the normal bundle and does not assert smoothness of the inverse tubular map.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.

theorem TauCeti.exists_isOpenEmbedding_normalTubeOfRadius {V : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ V] [I.Boundaryless] [IsManifold I 2 M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hind : Topology.IsInducing f) : ∃ (r : C(M, ℝ)), (∀ (x : M), 0 < r x) ∧ Topology.IsOpenEmbedding ((normalTubeOfRadius I f ⇑r).domRestrict fun (p : M × V) => f p.1 + p.2)

Noncompact Euclidean tubular neighbourhood theorem. A C² immersion inducing the source topology admits a positive continuous radius on which its normal addition map is an open embedding.