Integral curves through interior points on a compact time interval persist for nearby initial points

Let $M$ be a smooth 3-manifold with boundary (modelled on the closed half-space) and let $X$ be a C¹ vector field on $M$. An integral curve of $X$ on a set of times $S\subseteq\mathbb R$ is a curve $\gamma:\mathbb R\to M$ whose derivative within $S$ at every $u\in S$ is $X(\gamma(u))$ (Mathlib's IsMIntegralCurveOn; at the endpoints of an interval the derivative is one-sided). We write $[0,t]$ for the closed interval between $0$ and $t$, in either order (Mathlib's uIcc 0 t). Let $\gamma$ be an integral curve of $X$ on $[0,t]$ all of whose points $\gamma(s)$, $s\in[0,t]$, are interior points of $M$. Then every point $y$ in some neighbourhood of $\gamma(0)$ is the starting point of an integral curve of $X$ on $[0,t]$ through interior points: for all $y$ near $\gamma(0)$,

In words: orbits that stay in the interior of $M$ for a compact span of time persist for nearby initial points. This is the continuous dependence of solutions of a C¹ ordinary differential equation on initial conditions (continuation plus the Gronwall estimate in charts), restricted to what the formal development needs. 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 provides, for $y$ near a point of $\Lambda_X$, an orbit of $X$ that stays in the interior of $U$ up to time $t$, so that the time-$t$ map of the glued field $Z$ at $i_U(y)$ can be computed inside $U$.

Formalization Note No uniqueness is asserted and no Hausdorff or compactness hypothesis is assumed. Mathlib (at the pinned version) has short-time existence at interior points (exists_isMIntegralCurveAt_of_contMDiffAt) and, on boundaryless manifolds, global existence from a uniform existence time (exists_isMIntegralCurve_of_isMIntegralCurveOn); it has no continuous dependence on initial conditions, so existence on a prescribed compact time interval for nearby initial points is not available, which is why this statement is left open. C¹ is the mission's IsC1VectorField (the section $x\mapsto(x,X(x))$ of the tangent bundle is C¹). The conclusion is stated with Mathlib's ∀ᶠ y in 𝓝 (γ 0).