esp0_ext
plain-language theorem explainer
Two vectors in the ambient Euclidean line of the 0-sphere are equal once their single coordinate agrees. Anyone working with S⁰ as the unit sphere in ℝ¹ cites this to collapse pointwise data to a scalar identity. The proof is a short PiLp extensionality argument: the only Fin-index is 0, so the given coordinate equality is total equality.
Claim. Let $a,b\in\mathbb{R}^{1}$ (the ambient Euclidean space of $S^{0}$). If the unique coordinates agree, $a_{0}=b_{0}$, then $a=b$.
background
In this module the ambient space of the $n$-sphere is written $\mathrm{Esp},n:=\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin}(n+1))$, so $\mathrm{Esp},0$ is simply the Euclidean line $\mathbb{R}^{1}$ with a single coordinate indexed by $0\in\mathrm{Fin},1$. The $0$-sphere $\mathrm{Sph},0$ is the unit sphere in that line: the two points of norm one.
Coordinatewise equality of Euclidean-space vectors is the standard $\mathrm{PiLp}$ extensionality principle. In dimension zero there is only one index, so a single scalar hypothesis already determines the whole vector. The lemma is the $n=0$ special case of that principle, stated for the ambient type used throughout the singular-sphere geometry development.
proof idea
Apply $\mathrm{PiLp.ext}$ to reduce vector equality to agreement at every index $i:\mathrm{Fin},1$. For any such $i$, $\mathrm{Fin.ext}$ plus a trivial arithmetic check on the underlying naturals gives $i=0$. Rewrite the goal at that unique index and discharge it by the hypothesis $a,0=b,0$.
why it matters
The immediate consumer is $\mathrm{sph0_eq_pole}$: every point of $S^{0}$ is either the north or the south pole. That argument extracts the single ambient coordinate, squares it, and uses the unit-norm condition to force the coordinate to $\pm 1$; the present lemma turns that scalar dichotomy back into an equality of ambient (hence sphere) points.
In the broader Recognition geometry stack, $S^{0}$ is the base case of the singular-sphere hierarchy that supports charts, covers, and radial equivalences used in the foundation layer. Clean identification of the two poles keeps the $n=0$ case from becoming a special-case mess when the same constructions are later specialized or inducted upon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.