coverV
plain-language theorem explainer
The open set on the unit n-sphere obtained by deleting the north pole. It is the second chart in the standard two-set cover used for Mayer–Vietoris arguments on spheres in this module. Anyone citing the cover pair (U,V), the contractibility of the punctured sphere, or the H₁(S¹)≠0 argument will reference it. The body is a one-line set-theoretic complement.
Claim. For each $n\in\mathbb{N}$, write $S^n$ for the unit sphere in Euclidean space of dimension $n+1$. Let $N$ be the north pole (the last standard basis vector, viewed as a point of $S^n$). Then $\mathrm{coverV}(n)$ is the subset $S^n\setminus\{N\}$.
background
The ambient space is the unit sphere $S^n$ realized as a topological space: the set of unit vectors in $\mathbb{R}^{n+1}$ (here EuclideanSpace ℝ (Fin (n+1))), packaged as Sph n. The north pole is the point corresponding to the last standard basis vector; it is a concrete point of that sphere.
This module builds the classical two-chart cover of the sphere used in singular homology: one chart deletes the south pole, the other deletes the north pole. Their intersection is the doubly punctured sphere, which stereographic projection identifies with a punctured hyperplane. The local goal is to feed Mayer–Vietoris and extract that $H_1(S^1)$ is nonzero.
proof idea
Pure definition: the carrier set is the complement of the singleton consisting of the north pole inside the underlying set of the unit $n$-sphere. No lemmas are applied; openness, contractibility, and covering properties are proved separately.
why it matters
This set is half of the standard open cover of $S^n$. Downstream it appears in the union identity with the south-pole complement, the openness instance, the contractibility instance (punctured sphere is contractible), membership of the equatorial point in the intersection, the stereographic homeomorphism of the intersection onto a punctured hyperplane, and the Mayer–Vietoris exactness argument that $H_1(S^1)\neq 0$. In the Recognition foundation stack this is geometric scaffolding for the singular-sphere side of the forcing and homology arguments, not a physics constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.