A Hausdorff σ-compact 3-manifold with boundary carries a continuous Riemannian metric

Let $N$ be a Hausdorff, $\sigma$-compact smooth 3-manifold with boundary (modelled on the closed half-space). A continuous Riemannian metric $g$ on a 3-manifold $M$ is a continuously varying inner product $g_x$ on the tangent spaces $T_xM$ (Mathlib's Bundle.ContinuousRiemannianMetric on the tangent bundle; the mission's RiemannianMetric3), with norm $\|v\|_{g,x}=\sqrt{g_x(v,v)}$. Then $N$ carries a continuous Riemannian metric:

In words: every Hausdorff $\sigma$-compact 3-manifold with boundary admits a continuous Riemannian metric. The textbook proof glues the Euclidean inner products of the charts with a partition of unity; positivity is preserved because the set of positive definite symmetric bilinear forms is convex. A general fact, not stated in the paper; it is used tacitly in the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14), whose fourth and fifth sentences use, without comment, that the maximal invariant sets Λ_X and Λ_Y of the plugs (U, X) and (V, Y) are hyperbolic sets of the glued vector field Z with respect to some Riemannian metric on the glued manifold W. In the proof of the companion statement exists_comparable_metric it provides a metric on the glued manifold $W$.

Formalization Note The statement is Nonempty (RiemannianMetric3 N), where RiemannianMetric3 N is Bundle.ContinuousRiemannianMetric (EuclideanSpace ℝ (Fin 3)) (TangentSpace I3): a family of inner products on the tangent spaces, symmetric, positive definite, with bounded unit balls, continuous as a section of the bundle of bilinear forms. Only continuity is asked (no smoothness). $\sigma$-compactness and the Hausdorff property are what Mathlib's partition-of-unity theorems need; a compact manifold is $\sigma$-compact. Mathlib (at the pinned version) has no existence theorem for Riemannian metrics on manifolds, with or without boundary.