On a compact 3-manifold, a hyperbolic set is hyperbolic with respect to every continuous Riemannian metric

Let $M$ be a compact smooth 3-manifold with boundary (modelled on the closed half-space), let $X$ be a vector field on $M$ and let $\Lambda\subseteq M$ be a hyperbolic set of $X$. A set $\Lambda\subseteq M$ is a hyperbolic set of a vector field $X$ (the mission's IsHyperbolicSet X Λ) if there are a continuous Riemannian metric $g$, line fields $E^s$, $E^u$ on $\Lambda$ and constants $C>0$, $\lambda>0$ such that at every $x\in\Lambda$: $E^s_x\oplus\mathbb R X(x)\oplus E^u_x=T_xM$, the two line fields are invariant under the derivatives of the time-$t$ maps $\phi_t$ of the flow of $X$ for all $t\in\mathbb R$, and $\|D\phi_t(v)\|_g\le C e^{-\lambda t}\|v\|_g$ for $v\in E^s_x$, $t\ge0$, and $\|D\phi_{-t}(v)\|_g\le C e^{-\lambda t}\|v\|_g$ for $v\in E^u_x$, $t\ge0$. The time-$t$ map is the mission's flowMap X t, which sends $x$ to $\gamma(t)$ for a chosen integral curve $\gamma$ of $X$ on $[0,t]$ with $\gamma(0)=x$ when one exists, and to $x$ otherwise. 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 for every continuous Riemannian metric $g$ on $M$ there are line fields $E^s,E^u$ and constants $C>0$, $\lambda>0$ that satisfy the hyperbolicity conditions for $\Lambda$ with respect to $g$:

In words: on a compact manifold, hyperbolicity of a set does not depend on the choice of the continuous Riemannian metric. Only the constant $C$ changes. The proof compares the given metric with $g$ along the identity map (companion theorem comparable_of_metrics with $i=\mathrm{id}$): $c_1\|v\|_{g_0}\le\|v\|_g\le c_2\|v\|_{g_0}$ for all tangent vectors, and replaces $C$ by $C c_2/c_1$. It is used in the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14; GT 2017 Section 4.1). The proof of Proposition 1.1 needs the hyperbolic structures of the two pieces $i_U(\Lambda_X)$ and $i_V(\Lambda_Y)$ in one metric. The paper does not state this step.

Formalization Note The conclusion is the body of the mission's IsHyperbolicSet X Λ with the metric fixed to the given $g$ instead of existentially quantified; the exponent $\lambda$ may be kept. Compactness of $M$ is what makes the comparison constants uniform. The norm is the mission's RiemannianMetric3.norm, that is $\sqrt{g_x(v,v)}$.