seg_subset_range
plain-language theorem explainer
Any parameter subinterval of an arc on the sphere maps into the arc's full range. Algebraic topologists running the arc-complement acyclicity argument cite this when forming inclusions of complements of partial arcs. The proof is a one-line wrapper of the set fact that an image is contained in the range.
Claim. Let $a$ be an arc on the sphere $S^D$ and let $u,v\in\mathbb{R}$. Write $\mathrm{seg}(a;u,v)$ for the image under $a$ of $\{q\in I:u\le q\le v\}$. Then $\mathrm{seg}(a;u,v)\subseteq\mathrm{range}(a)$.
background
The module develops arc-complement acyclicity on the sphere $S^D$: every topological embedding of the unit interval has $H_1$-acyclic complement (Hatcher 2B.1, arc case). The ambient space is the unit sphere in Euclidean $D$-space, and arcs are continuous maps $a:I\to S^D$.
The local object is the partial arc image. For real bounds $u,v$, one takes the parameter set ${q\in I:u\le q\le v}$ and pushes it forward by $a$. That image is written $\mathrm{seg}(a;u,v)$ and is the set whose complement later carries a pushed reference 1-cycle.
Because $\mathrm{seg}$ is defined as an image under $a$, it is tautologically contained in the range of $a$. That containment is the only content of the present lemma; it licenses the continuous inclusion of the complement of the full arc into the complement of the partial segment.
proof idea
One-line wrapper. Unfolding the definition of $\mathrm{seg}$ exhibits it as $a''{\ldots}$, so the claim is exactly Set.image_subset_range applied to $a$ and the parameter subset. No topology or sphere structure is used.
why it matters
The lemma is the set-theoretic license for the partial-arc inclusion used throughout the bisection argument. Downstream, zSeg builds the pushforward of the reference cycle into the complement of $\mathrm{seg}(a;u,v)$ by composing with the chain map of the inclusion justified here. That non-boundary invariant is the bisection fuel for the main theorem arcComplementsAcyclic, which states that every embedded arc in $S^D$ has $H_1$-acyclic complement in every dimension $D$ (Hatcher 2B.1, arc case).
In the Recognition foundation stack this sits under linking-vanishing in high dimension: acyclicity of arc complements is the topological input that forces linking numbers (and related obstruction classes) to vanish once dimension is large enough. The lemma itself is pure set theory; its value is that it keeps the inclusion hypotheses of the chain-level constructions discharged without ad-hoc arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.