contractible_coverV
plain-language theorem explainer
Deleting the north pole from the unit sphere yields a contractible open chart. Anyone assembling a two-chart cover for homotopy or Čech arguments on the sphere cites this instance. The proof is a one-line specialization of the general fact that any punctured sphere is contractible via stereographic projection onto a hyperplane.
Claim. For every $n \in \mathbb{N}$, the set $S^n \setminus \{N\}$ (unit sphere in Euclidean space of dimension $n+1$, north pole $N$ removed) is a contractible topological space.
background
The module works with the unit sphere $\mathrm{Sph}, n$ in Euclidean space $\mathbb{R}^{n+1}$. Two poles are fixed, and the standard open cover is the pair of complementary charts: sphere minus south pole, and sphere minus north pole. The latter chart is exactly the set treated here.
Contractibility means homotopy-equivalent to a point. The upstream result records that any punctured sphere is contractible: "stereographic projection is a homeomorphism from the complement of a point onto the orthogonal hyperplane, which is a real topological vector space and hence contractible." This instance simply names that fact for the north-pole chart.
proof idea
One-line wrapper. The chart is definitionally the complement of the singleton north pole, so the general punctured-sphere contractibility theorem applies at that pole. That theorem matches the complement to the source of stereographic projection and inherits contractibility from the target hyperplane.
why it matters
Step 1 of the singular-sphere geometry development: each chart of the two-set open cover must be contractible so that the sphere's homotopy type is controlled by the intersection (the next section of the same module). In the Recognition foundation layer this geometry supports singular-sphere constructions used in topological and dimensional forcing (including the T8 step that forces $D=3$). No downstream consumers are wired yet; the instance is local infrastructure for the intersection analysis that follows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.