isClosed_seg
plain-language theorem explainer
On the unit D-sphere, the image of any closed parameter subinterval under a continuous arc is a closed set. Homology and bisection arguments for arc complements cite this whenever they need closedness of finite arc pieces. The proof is a short appeal to compactness of the segment plus the Hausdorff property of the sphere.
Claim. Let $a$ be a continuous arc on the unit sphere $S^{D}\subset\mathbb{R}^{D+1}$. For any $u,v\in\mathbb{R}$, the image $a(\{q\in I:\,u\le q\le v\})$ is a closed subset of $S^{D}$.
background
The ambient space is the unit sphere $\mathrm{Sph},D$ in Euclidean space $\mathrm{Esp},D=\mathbb{R}^{D+1}$, with $D=3$ forced by the Recognition forcing chain (T8 spatial dimension; T9 linking). An arc $a$ is a continuous map from the unit interval into that sphere. The segment $\mathrm{seg}(u,v)$ is the image under $a$ of the parameter set ${q\in I:u\le q\le v}$.
The sibling lemma isCompact_seg already shows that this image is compact: it is the continuous image of a closed (hence compact) subset of the unit interval. The present lemma upgrades compactness to closedness in the sphere topology.
The module develops acyclicity of arc complements, feeding high-dimensional linking-vanishing arguments imported from LinkingVanishingHighDim.
proof idea
Instantiate the Hausdorff (T2Space) structure on the underlying type of $\mathrm{Sph},D$ by identifying it with the unit sphere in $\mathrm{Esp},D$. In a Hausdorff space every compact set is closed, so apply IsCompact.isClosed to the already-proved compactness of $\mathrm{seg}(u,v)$. The argument is two lines: one instance inference, one exact application of the compact-implies-closed fact.
why it matters
Closedness of finite arc pieces is required by the bisection lemma bad_step: a "bad" parameter interval (one whose complement still carries a nontrivial 0-boundary class) has a bad half of half the length. That bisection is the engine of the arc-complement acyclicity argument in this module, which in turn supports high-dimensional linking vanishing.
In the Recognition chain this sits under the geometric side of T8/T9: spatial dimension $D=3$ is forced so that linking and sphere topology behave as needed. The lemma itself is pure point-set topology, but without it the closed-set hypotheses in the bad-interval calculus fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.