interHomeoPunctured
plain-language theorem explainer
Stereographic projection from the north pole restricts to a homeomorphism between the doubly punctured unit sphere S^n \ {N,S} and the punctured equatorial hyperplane Hyp \ {0}. Anyone building the two-chart cover of the singular sphere, or transferring path-connectedness and homotopy type off the intersection, cites this. The proof assembles Mathlib's stereographic homeomorphism with explicit forward/inverse maps and continuity via subtype and ContinuousOn composition.
Claim. For each $n \in \mathbb{N}$, stereographic projection from the north pole induces a homeomorphism $$S^n \setminus \{N,S\} \simeq_{\mathrm{top}} H_n \setminus \{0\},$$ where $S^n$ is the unit sphere in Euclidean space $\mathbb{R}^{n+1}$, $N$ and $S$ are the north and south poles, and $H_n$ is the orthogonal hyperplane to the north-pole axis (so the south pole maps to the origin).
background
The ambient space is Euclidean $\mathbb{R}^{n+1}$ (written Esp n), and Sph n is its unit sphere. The north-pole vector has norm one; the corresponding sphere points are the north and south poles $N$ and $S$, which are distinct.
Two open charts cover the sphere: the sphere minus the south pole, and the sphere minus the north pole. Their intersection is exactly the doubly punctured sphere ${x \in S^n : x \neq N,, x \neq S}$. The target space is the orthogonal complement $H_n$ of the north-pole line inside $\mathbb{R}^{n+1}$, viewed as the equatorial hyperplane for stereographic projection from $N$.
Mathlib supplies the stereographic homeomorphism from $S^n \setminus {N}$ onto $H_n$. Under that chart the south pole lands at the origin, so removing $S$ on the domain corresponds to removing $0$ on the codomain. That is the content packaged here.
proof idea
Fix the unit north-pole vector and Mathlib's stereographic chart at that pole. A short source lemma records that every sphere point other than $N$ lies in the chart domain.
Build a Homeomorph from an underlying Equiv:
- Forward: apply stereographic to the underlying sphere point; the image is nonzero because if it were $0$, injectivity of the chart on the source (together with stereographic of $S$ equaling $0$) would force the point to be $S$, contradicting membership in the intersection.
- Inverse: apply the chart inverse; the result is not $S$ for the dual reason (right-inverse plus stereographic of $S$ at $0$), and it is automatically not $N$ because it lands in the chart source.
- Left and right inverses are the chart's left/right inverses, pushed through subtype extensionality.
- Continuity of both directions is ContinuousOn of the chart (resp. its inverse) composed with subtype valuation, with the source/target membership obligations discharged by the intersection characterization and the fact that the stereographic target is the whole hyperplane.
why it matters
This is the geometric identification that turns the two-chart intersection on the singular sphere into a standard punctured Euclidean space. Downstream, interHomotopyEquiv composes it with polar coordinates on the punctured hyperplane and a linear isometry of that hyperplane onto $\mathbb{R}^n$, obtaining a homotopy equivalence
$$\mathrm{coverU}(n+1) \cap \mathrm{coverV}(n+1) \simeq S^n.$$
That is Step 2 of the singular-sphere cover analysis.
Separately, pathConnected_inter transports path-connectedness of $H_{n+2} \setminus {0}$ (available once the hyperplane rank exceeds one) across this homeomorphism, so the chart intersection is path-connected in the dimensions needed for linking-vanishing arguments.
In the broader Recognition foundation stack this sits under the singular-sphere geometry used for high-dimensional linking and cover arguments; it is pure differential topology scaffolding, not a forcing-chain (T0–T8) step, but it is the concrete homeomorphism those later homotopy and connectivity claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.