stereographic_source_pt
plain-language theorem explainer
Any point of the unit n-sphere other than a chosen base point p lies in the domain of the stereographic chart centered at p. Foundation workers cite this when building homeomorphisms of doubly punctured spheres for linking-vanishing arguments. The proof is a short rewrite of the chart-source definition followed by a subtype-equality contradiction with x ≠ p.
Claim. For every $n \in \mathbb{N}$, every $p \in S^n$, and every $x \in S^n$ with $x \neq p$, one has $x \in \mathrm{source}(\mathrm{stereographic}_p)$, where $\mathrm{stereographic}_p$ is the stereographic projection chart at $p$ (using $\|p\|=1$ in ambient Euclidean space).
background
In this module the n-sphere $S^n$ is the unit sphere in Euclidean space of dimension $n+1$ (as a topological space). Stereographic projection at a unit vector $v$ is the standard chart whose source is the sphere minus the chart pole; the ambient-norm lemma records that every sphere point has ambient norm one, so any $p \in S^n$ is a valid pole.
The sibling construction interHomeoPunctured already restricts stereographic projection at the north pole to a homeomorphism from the doubly punctured sphere onto the punctured hyperplane (south pole to the origin). The present lemma is the elementary membership fact needed to move that construction off the north pole to an arbitrary base point $p$.
Local setting is high-dimensional linking vanishing: one needs chart domains and homeomorphisms on $S^n \setminus {p,q}$ to control $H_1$ of arc complements.
proof idea
Rewrite the goal with the library characterization of the stereographic source (sphere minus the pole). The resulting membership statement says the ambient representative of $x$ equals that of $p$; packaging that equality as a subtype extensionality identity yields $x = p$, which contradicts the hypothesis $x \neq p$. Purely definitional; no geometric estimates.
why it matters
Feeds the definition twoPunctHomeo, which restricts stereographic projection at arbitrary $p$ to a homeomorphism $S^n \setminus {p,q} \simeq H_p \setminus {\mathrm{image}(q)}$, generalizing the north-pole homeomorphism interHomeoPunctured. That homeomorphism is the chart-level engine for high-dimensional linking-vanishing statements in this module (acyclicity of arc complements, detection of nontrivial linking). In the RS foundation stack this is geometric scaffolding under the forcing chain (T0–T8), not a direct claim about $J$, $\varphi$, or the eight-tick octave; it keeps the sphere geometry available when dimension arguments push past the low-dimensional linking cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.