Continuous radii for covers and diagonal neighbourhoods

A map inducing the topology from a pseudometric space admits a positive continuous radius. For each source point x, the preimage of the ball around f x with twice the chosen radius lies in one member of a prescribed open cover of the source. The radius can also be bounded by a positive constant assigned to that member. No local finiteness of the given cover or compactness of the source space is required.

This combines Mathlib's convex-valued partition-of-unity selection theorem exists_continuous_forall_mem_convex_of_local_const with metric balls. In tubular neighbourhood arguments, comparing the larger of two radii puts both base points in a single local injectivity neighbourhood.

An open family of diagonal neighbourhoods on a compact pseudometric space also admits a positive continuous radius over a normal paracompact parameter space, without compactness of that parameter space. This uses Mathlib's generalized tube lemma, its compact-space diagonal/uniformity comparison, and the same convex selection theorem. The radii control individual steps of local transports, without averaging invertible operators.

Similarly, an open subset of ℝ × X containing {0} × X contains a tube {(t, x) | |t| < ε x} of positive continuous width over a normal paracompact space X (IsOpen.exists_continuous_pos_forall_abs_lt). This is the shape of a collar of variable width around a noncompact hypersurface.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24, the variable-radius shrinking argument.

theorem Topology.IsInducing.exists_continuous_radius_subordinate {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace X] [PseudoMetricSpace Y] {f : X → Y} (hf : IsInducing f) (U : ι → Set X) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ∀ (x : X), ∃ (i : ι), x ∈ U i) (ε : ι → ℝ) (hε : ∀ (i : ι), 0 < ε i) : ∃ (r : C(X, ℝ)), (∀ (x : X), 0 < r x) ∧ ∀ (x : X), ∃ (i : ι), x ∈ U i ∧ r x < ε i ∧ ∀ (y : X), dist (f x) (f y) < 2 * r x → y ∈ U i

Choose positive continuous radii subordinate to an open cover of the source space. At each point, one cover member contains every point whose image is within twice the chosen radius, and its assigned positive bound exceeds that radius.

theorem IsOpen.exists_pos_forall_dist_le {X : Type u_1} {K : Type u_2} [TopologicalSpace X] [PseudoMetricSpace K] [CompactSpace K] {W : Set (X × K × K)} (hW : IsOpen W) (x : X) (hdiag : ∀ (s : K), (x, s, s) ∈ W) : ∃ ε > 0, ∀ᶠ (y : X) in nhds x, ∀ (s t : K), dist s t ≤ ε → (y, s, t) ∈ W

Near a parameter whose whole diagonal lies in an open set, one positive radius works uniformly for all pairs of sufficiently close points of the compact pseudometric space.

theorem IsOpen.exists_continuous_pos_forall_dist_le {X : Type u_1} {K : Type u_2} [TopologicalSpace X] [PseudoMetricSpace K] [CompactSpace K] {W : Set (X × K × K)} [NormalSpace X] [ParacompactSpace X] (hW : IsOpen W) (hdiag : ∀ (x : X) (s : K), (x, s, s) ∈ W) : ∃ (δ : C(X, ℝ)), (∀ (x : X), δ x ∈ Set.Ioo 0 1) ∧ ∀ (x : X) (s t : K), dist s t ≤ δ x → (x, s, t) ∈ W

An open family of diagonal neighbourhoods on a compact pseudometric space admits a continuous positive radius, bounded by one. No compactness assumption on the parameter space is needed.

theorem IsOpen.exists_continuous_pos_forall_abs_lt {X : Type u_1} [TopologicalSpace X] [NormalSpace X] [ParacompactSpace X] {U : Set (ℝ × X)} (hU : IsOpen U) (h0 : ∀ (x : X), (0, x) ∈ U) : ∃ (ε : C(X, ℝ)), (∀ (x : X), 0 < ε x) ∧ ∀ (x : X) (t : ℝ), |t| < ε x → (t, x) ∈ U

A tube of positive continuous width. Over a normal paracompact space X, an open subset of ℝ × X containing {0} × X contains the tube {(t, x) | |t| < ε x} of some positive continuous function ε. No compactness of X is needed.